Documentation

Lean 4 Proof

theorem symmetricShare_sum {J : ℕ} (hJ : 0 < J) :
    ∑ j : Fin J, symmetricShare J j = 1 := by
  simp only [symmetricShare, Finset.sum_const, Finset.card_fin]
  rw [nsmul_eq_mul]
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:446

Module Section

Information Geometry of CES:

In the same file