Documentation

Lean 4 Proof

private lemma hasDerivAt_rpow_exponent {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/InformationGeometry.lean:720

Module Section

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

In the same file