Documentation

Lean 4 Proof

theorem escortRawMoment_at_symmetry [NeZero J]
    {c : ℝ} (hc : 0 < c) (ρ : ℝ) (n : ℕ) :
    escortRawMoment (fun _ : Fin J => c) ρ n = (Real.log c) ^ n := by
  simp only [escortRawMoment, escortPartitionZn, escortPartitionZ]
  simp only [Finset.sum_const, Finset.card_fin, nsmul_eq_mul]
  have hcr : c ^ ρ ≠ 0 := ne_of_gt (rpow_pos_of_pos hc ρ)
  have hJ : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne J)
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CumulantTower.lean:286

Module Section

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

In the same file