Documentation

Lean 4 Proof

theorem prudence_locking [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    -- (i) kappa_3 is the derivative of kappa_2
    HasDerivAt (fun p => escortCumulant2 x p) (escortCumulant3 x ρ) ρ ∧
    -- (ii) Both vanish at symmetry
    (∀ c : ℝ, 0 < c →
      escortCumulant2 (fun _ : Fin J => c) ρ = 0 ∧
      escortCumulant3 (fun _ : Fin J => c) ρ = 0) :=
  ⟨cumulant3_is_derivative_of_variance x hx ρ,
   fun _ hc => ⟨escortCumulant2_zero_at_symmetry hc ρ,
                 escortCumulant3_zero_at_symmetry hc ρ⟩⟩

Dependency Graph

Location

thesis/CESProofs/Foundations/CumulantTower.lean:443

Module Section

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

In the same file