English
For an orthogonal family, the norm of a sum difference equals the sum of squared norms of the differing indices.
Русский
Для ортогонального семейства норма разности сумм равна сумме квадратов норм соответствующих индексов.
LaTeX
$$$\|\sum_{i\in s_1} V_i(f_i) - \sum_{i\in s_2} V_i(f_i)\|^2 = \sum_{i\in s_1\setminus s_2} \|f_i\|^2 + \sum_{i\in s_2\setminus s_1} \|f_i\|^2$$$
Lean4
theorem norm_sq_diff_sum [DecidableEq ι] (f : ∀ i, G i) (s₁ s₂ : Finset ι) :
‖(∑ i ∈ s₁, V i (f i)) - ∑ i ∈ s₂, V i (f i)‖ ^ 2 = (∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2) + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2 :=
by
rw [← Finset.sum_sdiff_sub_sum_sdiff, sub_eq_add_neg, ← Finset.sum_neg_distrib]
let F : ∀ i, G i := fun i => if i ∈ s₁ then f i else -f i
have hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i := fun i hi => if_pos (Finset.sdiff_subset hi)
have hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i := fun i hi => if_neg (Finset.mem_sdiff.mp hi).2
have hF : ∀ i, ‖F i‖ = ‖f i‖ := by
intro i
dsimp only [F]
split_ifs <;> simp only [norm_neg]
have :
‖(∑ i ∈ s₁ \ s₂, V i (F i)) + ∑ i ∈ s₂ \ s₁, V i (F i)‖ ^ 2 =
(∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2) + ∑ i ∈ s₂ \ s₁, ‖F i‖ ^ 2 :=
by
have hs : Disjoint (s₁ \ s₂) (s₂ \ s₁) := disjoint_sdiff_sdiff
simpa only [Finset.sum_union hs] using hV.norm_sum F (s₁ \ s₂ ∪ s₂ \ s₁)
convert this using 4
· refine Finset.sum_congr rfl fun i hi => ?_
simp only [hF₁ i hi]
· refine Finset.sum_congr rfl fun i hi => ?_
simp only [hF₂ i hi, LinearIsometry.map_neg]
· simp only [hF]
· simp only [hF]
