Source indexedlemma · leanprover/lean4:v4.33.0-rc1

offDiag_sum_left

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:1018 to 1028

Mathematical statement

Exact Lean statement

lemma offDiag_sum_left {m : ℕ} (hm : 1 ≤ m) (f : Fin m → ℝ) :
    offDiag_sum (fun j _ ↦ f j) = (m - 1) * ∑ j, f j

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma offDiag_sum_left {m : ℕ} (hm : 1 ≤ m) (f : Fin m → ℝ) :    offDiag_sum (fun j _ ↦ f j) = (m - 1) * ∑ j, f j := by  rw [Finset.mul_sum]  congr! with j hj  simp only [Finset.sum_ite, Finset.sum_const_zero, Finset.sum_const, nsmul_eq_mul, zero_add,    mul_eq_mul_right_iff]  left  have : Finset.filter (fun x ↦ ¬j = x)  Finset.univ = Finset.univ.erase j := by aesop  rw [this, Finset.card_erase_of_mem hj, Finset.card_univ, Fintype.card_fin]  convert Nat.cast_sub hm  simp only [Nat.cast_one]