Documentation

Lean 4 Proof

theorem escortRawMoment_zero [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    escortRawMoment x ρ 0 = 1 := by
  simp only [escortRawMoment, escortPartitionZn_zero]
  exact div_self (ne_of_gt (escortPartitionZ_pos x hx ρ))

Dependency Graph

Location

thesis/CESProofs/Foundations/CumulantTower.lean:114

Module Section

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

In the same file