Documentation

Lean 4 Proof

theorem escortRawMoment_one [NeZero J]
    (x : Fin J → ℝ) (_hx : ∀ j, 0 < x j) (ρ : ℝ) :
    escortRawMoment x ρ 1 =
    escortExpectation x ρ (fun j => Real.log (x j)) := by
  simp only [escortRawMoment, escortPartitionZn, escortExpectation,
    escortProbability, pow_one, div_mul_eq_mul_div, ← Finset.sum_div]

Dependency Graph

Location

thesis/CESProofs/Foundations/CumulantTower.lean:121

Module Section

The Cumulant Tower: Higher-Order Bridges Between CES and Escort Statistics

In the same file