Documentation

Lean 4 Proof

theorem escortExpectation_eq_sum_div [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j)
    (ρ : ℝ) (f : Fin J → ℝ) :
    escortExpectation x ρ f =
      (∑ j, x j ^ ρ * f j) / escortPartitionZ x ρ := by
  unfold escortExpectation escortProbability
  simp_rw [div_mul_eq_mul_div]
  rw [← Finset.sum_div]

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:768

Module Section

The VRI σ² = T·χ is fundamentally an exponential family identity:

In the same file