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 (finset.univ.sum (λ (i : n), α i ^ 2)) = finset.univ.sum (λ (i : n), ⇑complex.abs (α i) ^ 2) ↔ ∀ (i j : n), (α i).re * (α j).im = (α j).re * (α i).im

$| \sum_{i} α_{i}^{2} | = \sum_{i} | α_{i} |^{2}$ if and only if $\forall i, j \in [n] : ℜ (α_{i}) ℑ (α_{j}) = ℜ (α_{j}) ℑ (α_{i})$

source

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

source

theorem abs_of_sq_add_sq_abs_sq_add_abs_sq_iff' (α₁ α₂ : ℂ) :

⇑complex.abs (α₁ ^ 2 + α₂ ^ 2) = ⇑complex.abs α₁ ^ 2 + ⇑complex.abs α₂ ^ 2 ↔ α₁ * ⇑(star_ring_end ℂ) α₂ = ⇑(star_ring_end ℂ) α₁ * α₂

source

theorem abs_of_sum_sq_eq_sum_abs_sq_iff' {n : Type u_1} [fintype n] (α : n → ℂ) :

⇑complex.abs (finset.univ.sum (λ (i : n), α i ^ 2)) = finset.univ.sum (λ (i : n), ⇑complex.abs (α i) ^ 2) ↔ ∀ (i j : n), α i * ⇑(star_ring_end ℂ) (α j) = ⇑(star_ring_end ℂ) (α i) * α j

$| \sum_{i} α_{i}^{2} | = \sum_{i} | α_{i} |^{2}$ is also equivalent to saying that for any $i, j$ we get $α_{i} \overset{―}{α_{j}} = \overset{―}{α_{i}} α_{j}$

source

theorem abs_of_sq_add_sq_abs_sq_add_abs_sq_iff'' (α₁ α₂ : ℂ) :

⇑complex.abs (α₁ ^ 2 + α₂ ^ 2) = ⇑complex.abs α₁ ^ 2 + ⇑complex.abs α₂ ^ 2 ↔ ∃ (γ : ℂ) (β₁ β₂ : ℝ), α₁ = γ * ↑β₁ ∧ α₂ = γ * ↑β₂

source

theorem abs_of_sum_sq_eq_sum_abs_sq_iff'' {n : Type u_1} [fintype n] (α : n → ℂ) :

⇑complex.abs (finset.univ.sum (λ (i : n), α i ^ 2)) = finset.univ.sum (λ (i : n), ⇑complex.abs (α i) ^ 2) ↔ ∃ (γ : ℂ), ∀ (i : n), ∃ (β : ℝ), α i = γ * ↑β

$| \sum_{i} α_{i}^{2} | = \sum_{i} | α_{i} |^{2}$ is equivalent to saying that there exists some $γ \in C$ such that for any $i \in [n]$ we get there exists some $β \in R$ such that $α_{i} = γ β$