Documentation

Lean 4 Proof

theorem cumulant_tower_summary [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    -- (i) Moment recursion holds for all n
    (∀ n, HasDerivAt (fun p => escortRawMoment x p n)
      (escortRawMoment x ρ (n + 1) -
       escortRawMoment x ρ n * escortRawMoment x ρ 1) ρ) ∧
    -- (ii) kappa_2 = d/drho M_1 (VRI)
    HasDerivAt (fun p => escortRawMoment x p 1)
      (escortCumulant2 x ρ) ρ ∧
    -- (iii) kappa_3 = d/drho kappa_2
    HasDerivAt (fun p => escortCumulant2 x p)
      (escortCumulant3 x ρ) ρ ∧
    -- (iv) kappa_4 = d/drho kappa_3
    HasDerivAt (fun p => escortCumulant3 x p)
      (escortCumulant4 x ρ) ρ ∧
    -- (v) All cumulants vanish at symmetry
    (∀ c : ℝ, 0 < c →
      escortCumulant2 (fun _ : Fin J => c) ρ = 0 ∧
      escortCumulant3 (fun _ : Fin J => c) ρ = 0 ∧
      escortCumulant4 (fun _ : Fin J => c) ρ = 0) :=
  ⟨fun n => escortRawMoment_hasDerivAt x hx ρ n,
   vri_from_moment_recursion x hx ρ,
   cumulant3_is_derivative_of_variance x hx ρ,
   cumulant4_is_derivative_of_cumulant3 x hx ρ,
   fun _ hc => ⟨escortCumulant2_zero_at_symmetry hc ρ,
                 escortCumulant3_zero_at_symmetry hc ρ,
                 escortCumulant4_zero_at_symmetry hc ρ⟩⟩

Dependency Graph

Location

thesis/CESProofs/Foundations/CumulantTower.lean:476

Module Section

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

In the same file