Documentation

Lean 4 Proof

theorem escort_expectation_const [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) (c : ℝ) :
    escortExpectation x ρ (fun _ => c) = c := by
  unfold escortExpectation
  simp_rw [mul_comm _ c, ← Finset.mul_sum]
  rw [escort_prob_sum_one x hx ρ, mul_one]

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:931

Module Section

### Part F: The Dual Curvature Principle

In the same file