Documentation

Lean 4 Proof

private lemma hasDerivAt_rpow {x : ℝ} (hx : 0 < x) (ρ : ℝ) :
    HasDerivAt (fun p => x ^ p) (x ^ ρ * Real.log x) ρ := by
  simp_rw [rpow_def_of_pos hx]
  exact ((hasDerivAt_id ρ).const_mul (Real.log x)
    |>.congr_deriv (by ring)).exp

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CumulantTower.lean:47

Module Section

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

In the same file