Sections / Section 6: Information Geometry and Cumulant Tower / escortCumulant2_zero_at_symmetry

Escort Cumulant 2 Zero At Symmetry

theoremprovedInfo Geometrykey theorem

Documentation

Lean 4 Proof

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

Dependency Graph

Used by

cumulant_tower_summary prudence_locking

Location

thesis/CESProofs/Foundations/CumulantTower.lean:315

Module Section

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

In the same file

hasDerivAt_rpow hasDerivAt_rpow_logpow escortPartitionZn escortPartitionZn_zero escortPartitionZn_one escortPartitionZn_hasDerivAt escortRawMoment escortRawMoment_zero escortRawMoment_one escortRawMoment_hasDerivAt escortCumulant2 escortCumulant3 escortCumulant4 escortCumulant2_eq_variance cumulant3_is_derivative_of_variance cumulant4_is_derivative_of_cumulant3 escortRawMoment_at_symmetry escortCumulant3_zero_at_symmetry escortCumulant4_zero_at_symmetry escortCentralMoment