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

Escort Cumulant 3

defprovedInfo Geometry

Documentation

Lean 4 Proof

def escortCumulant3 (x : Fin J → ℝ) (ρ : ℝ) : ℝ :=
  escortRawMoment x ρ 3 - 3 * escortRawMoment x ρ 2 * escortRawMoment x ρ 1
    + 2 * escortRawMoment x ρ 1 ^ 3

Dependency Graph

Used by

cumulant_tower_summary cumulant4_is_derivative_of_cumulant3 escortCumulant3_zero_at_symmetry cumulant3_is_derivative_of_variance prudence_locking

Location

thesis/CESProofs/Foundations/CumulantTower.lean:178

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 escortCumulant4 escortCumulant2_eq_variance cumulant3_is_derivative_of_variance cumulant4_is_derivative_of_cumulant3 escortRawMoment_at_symmetry escortCumulant2_zero_at_symmetry escortCumulant3_zero_at_symmetry escortCumulant4_zero_at_symmetry escortCentralMoment