Documentation

Lean 4 Proof

theorem perCapitaSurplus_decreasing_above_peak {J₁ J₂ ρ : ℝ}
    (hJ₁ : 2 ≤ J₁) (hJ₁₂ : J₁ < J₂) (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ξ_neg : perCapitaSurplusDeriv ξ ρ < 0 :=
    perCapitaSurplusDeriv_neg (by linarith [hξ.1]) hρ
  rw [hslope] at hξ_neg
  have hd : (0:ℝ) < J₂ - J₁ := by linarith
  have hVdiff : perCapitaSurplus J₂ ρ - perCapitaSurplus J₁ ρ < 0 := by
    by_contra h_not
    push_neg at h_not
    have : 0 ≤ (perCapitaSurplus J₂ ρ - perCapitaSurplus J₁ ρ) / (J₂ - J₁) :=
      div_nonneg h_not (le_of_lt hd)
    linarith
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Calculus.lean:261

Module Section

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

In the same file