Source indexedlemma · leanprover/lean4:v4.32.0

Finset.sum_range_mul_conj_sum_range

Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:747 to 758

Mathematical statement

Exact Lean statement

lemma Finset.sum_range_mul_conj_sum_range {α : Type*} {s : Finset α} {f : α → ℂ} :
    ∑ j ∈ s, f j * conj (f j) + ∑ j ∈ s, ∑ j' ∈ s with j ≠ j', f j * conj (f j') =
    (∑ j ∈ s, f j) * conj (∑ j' ∈ s, f j')

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Finset.sum_range_mul_conj_sum_range {α : Type*} {s : Finset α} {f : α → ℂ} :    ∑ j ∈ s, f j * conj (f j) + ∑ j ∈ s, ∑ j' ∈ s with j ≠ j', f j * conj (f j') =    (∑ j ∈ s, f j) * conj (∑ j' ∈ s, f j') := by  calc    _ = ∑ j ∈ s, ∑ j' ∈ s with j = j', f j * conj (f j') +        ∑ j ∈ s, ∑ j' ∈ s with j ≠ j', f j * conj (f j') := by      rw [add_left_inj]      congr! with j mj; simp_rw [filter_eq, mj, ite_true, sum_singleton]    _ = _ := by      conv_lhs =>        rw [← sum_add_distrib]; enter [2, j]; rw [sum_filter_add_sum_filter_not, ← mul_sum]      rw [sum_mul, map_sum]