Documentation

Lean 4 Proof

theorem perCapitaSurplus_increasing_below_peak {J₁ J₂ ρ : ℝ}
    (hJ₁ : 1 < J₁) (hJ₁₂ : J₁ < J₂) (hJ₂ : J₂ ≤ 2) (hρ : ρ < 1) :
    perCapitaSurplus J₁ ρ < perCapitaSurplus J₂ ρ := by
  have hcont : ContinuousOn (fun x => perCapitaSurplus x ρ) (Set.Icc J₁ J₂) := by
    simp only [perCapitaSurplus]
    apply ContinuousOn.div
    · exact continuousOn_const.mul (continuousOn_id.sub continuousOn_const)
    · exact (continuousOn_id.pow 2)
    · intro x hx; exact ne_of_gt (pow_pos (by linarith [hx.1]) 2)
  have hdiff : ∀ x ∈ Set.Ioo J₁ J₂,
      HasDerivAt (fun J => perCapitaSurplus J ρ) (perCapitaSurplusDeriv x ρ) x :=
    fun x hx => hasDerivAt_perCapitaSurplus (by linarith [hx.1])
  obtain ⟨ξ, hξ, hslope⟩ := exists_hasDerivAt_eq_slope
    (fun J => perCapitaSurplus J ρ) (fun x => perCapitaSurplusDeriv x ρ)
    (by linarith) hcont hdiff
  have hξ_pos : 0 < perCapitaSurplusDeriv ξ ρ :=
    perCapitaSurplusDeriv_pos (by linarith [hξ.1]) (by linarith [hξ.2]) hρ
  rw [hslope] at hξ_pos
  linarith [div_pos_iff_of_pos_right (show (0:ℝ) < J₂ - J₁ by linarith) |>.mp hξ_pos]

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Calculus.lean:240

Module Section

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

In the same file