Documentation

Lean 4 Proof

theorem hasDerivAt_perCapitaSurplus {J ρ : ℝ} (hJ : 0 < J) :
    HasDerivAt (fun x => perCapitaSurplus x ρ) (perCapitaSurplusDeriv J ρ) J := by
  have hJne : J ≠ 0 := ne_of_gt hJ
  -- Rewrite π_K as (1-ρ) * ((J-1)/J²) = (1-ρ) * (J⁻¹ - J⁻²)
  -- But J⁻² is not standard. Instead rewrite K(J) = (1-ρ) - (1-ρ)/J
  -- and K(J)/J = ((1-ρ) - (1-ρ)/J)/J = (1-ρ)/J - (1-ρ)/J²
  -- Use EventuallyEq to rewrite the function
  have heq : (nhds J).EventuallyEq
      (fun x => perCapitaSurplus x ρ)
      (fun x => (1 - ρ) * x⁻¹ - (1 - ρ) * (x⁻¹ * x⁻¹)) := by
    filter_upwards [IsOpen.mem_nhds isOpen_ne hJne] with x hx
    simp only [perCapitaSurplus]
    field_simp
  rw [heq.hasDerivAt_iff]
  -- d/dx[x⁻¹] = -x⁻²
  have hinv := hasDerivAt_inv hJne  -- d[x⁻¹] = -(J^2)⁻¹
  -- d/dx[x⁻¹ * x⁻¹] = 2 * x⁻¹ * (-(J^2)⁻¹) by product rule
  have hinv2 := hinv.mul hinv  -- d[x⁻¹ · x⁻¹]
  -- Combine
  have h1 := hinv.const_mul (1 - ρ)
  have h2 := hinv2.const_mul (1 - ρ)
  convert h1.sub h2 using 1
  simp only [perCapitaSurplusDeriv]
  field_simp
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Calculus.lean:197

Module Section

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

In the same file