Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Foundations/CumulantTower.lean:206

Module Section

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

In the same file