Documentation

Lean 4 Proof

private lemma hasDerivAt_rpow_exponent_sq {x : ℝ}
    (hx : 0 < x) (ρ : ℝ) :
    HasDerivAt (fun p => x ^ p * Real.log x)
      (x ^ ρ * (Real.log x) ^ 2) ρ := by
  convert (hasDerivAt_rpow_exponent hx ρ).mul_const
    (Real.log x) using 1
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:729

Module Section

The VRI σ² = T·χ is fundamentally an exponential family identity:

In the same file