Documentation

Lean 4 Proof

theorem cumulant4_is_derivative_of_cumulant3 [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    HasDerivAt (fun p => escortCumulant3 x p)
      (escortCumulant4 x ρ) ρ := by
  unfold escortCumulant3 escortCumulant4
  have hM := fun n => escortRawMoment_hasDerivAt x hx ρ n
  -- kappa_3 = M_3 - 3*M_2*M_1 + 2*M_1^3
  -- Build HasDerivAt in left-associative order to match function syntax:
  -- Term 1: M_3
  -- Term 2: 3*M_2*M_1 (build as (const_mul 3 of M_2).mul M_1)
  -- Term 3: 2*M_1^3 (build as (pow 3 of M_1).const_mul 2)
  have h := (hM 3).sub (((hM 2).const_mul 3).mul (hM 1))
    |>.add (((hM 1).pow 3).const_mul 2)
  refine h.congr_deriv ?_
  simp only [Nat.cast_ofNat]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CumulantTower.lean:260

Module Section

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

In the same file