Documentation

Lean 4 Proof

theorem perCapitaSurplusDeriv_neg {J ρ : ℝ} (hJ : 2 < J) (hρ : ρ < 1) :
    perCapitaSurplusDeriv J ρ < 0 := by
  simp only [perCapitaSurplusDeriv]
  apply div_neg_of_neg_of_pos
  · exact mul_neg_of_pos_of_neg (by linarith) (by linarith)
  · exact pow_pos (by linarith) 3

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Calculus.lean:232

Module Section

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

In the same file