Documentation

Lean 4 Proof

theorem ces_partition_identity_restated [NeZero J] {ρ : ℝ} (hρ : ρ ≠ 0)
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) :
    ρ * Real.log (powerMean J ρ hρ x) =
    Real.log (escortPartitionZ x ρ) - Real.log ↑J :=
  logCES_eq_logPartition hρ x hx

Dependency Graph

Location

thesis/CESProofs/Foundations/CumulantTower.lean:410

Module Section

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

In the same file