Documentation

Lean 4 Proof

theorem escort_prob_sum_one [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    ∑ j : Fin J, escortProbability x ρ j = 1 := by
  unfold escortProbability escortPartitionZ
  rw [← Finset.sum_div, div_self
    (ne_of_gt (sum_pos (fun j _ => rpow_pos_of_pos (hx j) ρ)
      Finset.univ_nonempty))]

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:918

Module Section

### Part F: The Dual Curvature Principle

In the same file