Documentation

Lean 4 Proof

theorem escortPartitionZn_hasDerivAt
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) (n : ℕ) :
    HasDerivAt (fun p => escortPartitionZn x p n)
      (escortPartitionZn x ρ (n + 1)) ρ := by
  unfold escortPartitionZn
  convert HasDerivAt.sum (u := Finset.univ)
    (fun j _ => hasDerivAt_rpow_logpow (hx j) ρ n) using 1
  ext p; simp

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CumulantTower.lean:89

Module Section

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

In the same file