Documentation

Lean 4 Proof

theorem hasDerivAt_curvatureK_real {J ρ : ℝ} (hJ : J ≠ 0) :
    HasDerivAt (fun x => curvatureKReal x ρ) (marginalK J ρ) J := by
  simp only [curvatureKReal, marginalK]
  have heq : (nhds J).EventuallyEq
      (fun x => (1 - ρ) * (x - 1) / x)
      (fun x => (1 - ρ) - (1 - ρ) * x⁻¹) := by
    filter_upwards [IsOpen.mem_nhds isOpen_ne hJ] with x hx; field_simp
  rw [heq.hasDerivAt_iff]
  convert (hasDerivAt_const J (1 - ρ)).sub ((hasDerivAt_inv hJ).const_mul (1 - ρ)) using 1
  field_simp; ring

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Calculus.lean:27

Module Section

Paper 1c: Formal Calculus on K(J) and V(J)

In the same file