Lean 4 Proof

theorem escortCumulant4_zero_at_symmetry [NeZero J]
    {c : ℝ} (hc : 0 < c) (ρ : ℝ) :
    escortCumulant4 (fun _ : Fin J => c) ρ = 0 := by
  simp only [escortCumulant4, escortRawMoment_at_symmetry hc]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CumulantTower.lean:327

Module Section

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

In the same file