Documentation

Lean 4 Proof

private lemma hasDerivAt_rpow_logpow {x : ℝ} (hx : 0 < x) (ρ : ℝ) (n : ℕ) :
    HasDerivAt (fun p => x ^ p * (Real.log x) ^ n)
      (x ^ ρ * (Real.log x) ^ (n + 1)) ρ := by
  convert (hasDerivAt_rpow hx ρ).mul_const ((Real.log x) ^ n) using 1
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CumulantTower.lean:58

Module Section

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

In the same file