Documentation

Lean 4 Proof

theorem welfareDistanceFn_deriv {z : ℝ} (hz : z ≠ 0) :
    HasDerivAt welfareDistanceFn (1 - z⁻¹) z := by
  change HasDerivAt (fun z => z - 1 - Real.log z) (1 - z⁻¹) z
  have h := ((hasDerivAt_id z).sub (hasDerivAt_const z 1)).sub
    (Real.hasDerivAt_log hz)
  convert h using 1
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:124

Module Section

Information Geometry of CES:

In the same file