Some stuff about complex numbers

This file contains some basic lemmas about complex numbers.

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

The norm of ∑ i, α i ^ 2 is the sum of ‖α i‖ ^ 2 if and only if the real and imaginary parts of the α i are pairwise proportional.

theorem norm_of_sq_add_sq_eq_norm_sq_add_norm_sq_iff (α₁ α₂ : ℂ) : ‖α₁ ^ 2 + α₂ ^ 2‖ = ‖α₁‖ ^ 2 + ‖α₂‖ ^ 2 ↔ α₁.re * α₂.im = α₂.re * α₁.im

theorem norm_of_sq_add_sq_norm_sq_add_norm_sq_iff' (α₁ α₂ : ℂ) : ‖α₁ ^ 2 + α₂ ^ 2‖ = ‖α₁‖ ^ 2 + ‖α₂‖ ^ 2 ↔ α₁ * (starRingEnd ℂ) α₂ = (starRingEnd ℂ) α₁ * α₂

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

The norm identity for a finite sum of squares is equivalent to saying that α i * conj (α j) = conj (α i) * α j for every pair i, j.

theorem norm_of_sq_add_sq_norm_sq_add_norm_sq_iff'' (α₁ α₂ : ℂ) : ‖α₁ ^ 2 + α₂ ^ 2‖ = ‖α₁‖ ^ 2 + ‖α₂‖ ^ 2 ↔ ∃ (γ : ℂ) (β₁ : ℝ) (β₂ : ℝ), α₁ = γ * ↑β₁ ∧ α₂ = γ * ↑β₂

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

The norm identity for a finite sum of squares is equivalent to all α i lying on a common complex line through the origin with real coefficients.