Documentation

Lean 4 Proof

theorem welfareDistanceFn_second_deriv {z : ℝ} (hz : z ≠ 0) :
    HasDerivAt (fun z => 1 - z⁻¹) ((z ^ 2)⁻¹) z := by
  have h := (hasDerivAt_const z (1 : ℝ)).sub ((hasDerivAt_id z).inv hz)
  simp only [id] at h
  convert h using 1
  have hz2 : z ^ 2 ≠ 0 := pow_ne_zero 2 hz
  field_simp
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:142

Module Section

Information Geometry of CES:

In the same file