Some stuff about complex numbers

This file contains some basic lemmas about complex numbers.

theorem abs_of_sum_sq_eq_sum_abs_sq_iff {n : Type u_1} [Fintype n] (α : n → ℂ) : Complex.abs (∑ i : n, α i ^ 2) = ∑ i : n, Complex.abs (α i) ^ 2 ↔ ∀ (i j : n), (α i).re * (α j).im = (α j).re * (α i).im

$\left|\sum_i\alpha_i^2\right|=\sum_i|\alpha_i|^2$ if and only if $\forall{i,j}\in[n]:\Re(\alpha_i)\Im(\alpha_j)=\Re(\alpha_j)\Im(\alpha_i)$

theorem abs_of_sq_add_sq_eq_abs_sq_add_abs_sq_iff (α₁ : ℂ) (α₂ : ℂ) : Complex.abs (α₁ ^ 2 + α₂ ^ 2) = Complex.abs α₁ ^ 2 + Complex.abs α₂ ^ 2 ↔ α₁.re * α₂.im = α₂.re * α₁.im

theorem abs_of_sq_add_sq_abs_sq_add_abs_sq_iff' (α₁ : ℂ) (α₂ : ℂ) : Complex.abs (α₁ ^ 2 + α₂ ^ 2) = Complex.abs α₁ ^ 2 + Complex.abs α₂ ^ 2 ↔ α₁ * (starRingEnd ℂ) α₂ = (starRingEnd ℂ) α₁ * α₂

theorem abs_of_sum_sq_eq_sum_abs_sq_iff' {n : Type u_1} [Fintype n] (α : n → ℂ) : Complex.abs (∑ i : n, α i ^ 2) = ∑ i : n, Complex.abs (α i) ^ 2 ↔ ∀ (i j : n), α i * (starRingEnd ℂ) (α j) = (starRingEnd ℂ) (α i) * α j

$\left|\sum_i\alpha_i^2\right|=\sum_i|\alpha_i|^2$ is also equivalent to saying that for any $i,j$ we get $\alpha_i\overline{\alpha_j}=\overline{\alpha_i}\alpha_j$

theorem abs_of_sq_add_sq_abs_sq_add_abs_sq_iff'' (α₁ : ℂ) (α₂ : ℂ) : Complex.abs (α₁ ^ 2 + α₂ ^ 2) = Complex.abs α₁ ^ 2 + Complex.abs α₂ ^ 2 ↔ ∃ (γ : ℂ) (β₁ : ℝ) (β₂ : ℝ), α₁ = γ * ↑β₁ ∧ α₂ = γ * ↑β₂

theorem abs_of_sum_sq_eq_sum_abs_sq_iff'' {n : Type u_1} [Fintype n] (α : n → ℂ) : Complex.abs (∑ i : n, α i ^ 2) = ∑ i : n, Complex.abs (α i) ^ 2 ↔ ∃ (γ : ℂ), ∀ (i : n), ∃ (β : ℝ), α i = γ * ↑β

$\left|\sum_i\alpha_i^2\right|=\sum_i|\alpha_i|^2$ is equivalent to saying that there exists some $\gamma\in\mathbb{C}$ such that for any $i\in[n]$ we get there exists some $\beta\in\mathbb{R}$ such that $\alpha_i=\gamma\beta$