Documentation

Lean 4 Proof

theorem escortCentralMoment_zero_at_symmetry [NeZero J]
    {c : ℝ} (hc : 0 < c) (ρ : ℝ) {n : ℕ} (hn : 1 ≤ n) :
    escortCentralMoment (fun _ : Fin J => c) ρ n = 0 := by
  unfold escortCentralMoment
  -- The mean is log c
  have hmean : escortExpectation (fun _ : Fin J => c) ρ
      (fun _ => Real.log c) = Real.log c :=
    escort_expectation_const _ (fun _ => hc) ρ (Real.log c)
  -- Simplify: log(c) for constant input
  simp only [hmean, sub_self, zero_pow (by omega : n ≠ 0)]
  exact escort_expectation_const _ (fun _ => hc) ρ 0

Dependency Graph

Location

thesis/CESProofs/Foundations/CumulantTower.lean:358

Module Section

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

In the same file