Documentation

Lean 4 Proof

theorem curvatureK_increment {J : ℕ} {ρ : ℝ} (hJ : 0 < J) :
    curvatureK (J + 1) ρ - curvatureK J ρ = (1 - ρ) / (↑J * (↑J + 1)) := by
  simp only [curvatureK]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hJ)
  have hJ1ne : (↑J : ℝ) + 1 ≠ 0 := by positivity
  push_cast
  field_simp [hJne, hJ1ne]
  ring

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:385

Module Section

Economics extensions for CES formalization:

In the same file