Documentation

Lean 4 Proof

theorem perCapitaSurplus_le_peak {J ρ : ℝ} (hJ : 1 < J) (hρ : ρ < 1) :
    perCapitaSurplus J ρ ≤ (1 - ρ) / 4 := by
  rw [← perCapitaSurplus_at_two ρ]
  by_cases h2 : J ≤ 2
  · rcases (lt_or_eq_of_le h2) with hlt | heq
    · exact le_of_lt (perCapitaSurplus_increasing_below_peak hJ hlt le_rfl hρ)
    · rw [heq]
  · push_neg at h2
    exact le_of_lt (perCapitaSurplus_decreasing_above_peak le_rfl h2 hρ)

Dependency Graph

Location

thesis/CESProofs/EntryExit/Calculus.lean:291

Module Section

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

In the same file