Documentation

Lean 4 Proof

theorem valueFunction_increasing {J₁ J₂ ρ c : ℝ}
    (hJ₁ : 1 < J₁) (hJ₁₂ : J₁ < J₂) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hc : 0 < c) :
    valueFunction J₁ ρ c < valueFunction J₂ ρ c := by
  have hJ₁pos : 0 < J₁ := by linarith
  have hJ₂pos : 0 < J₂ := by linarith
  -- Apply MVT: there exists ξ ∈ (J₁, J₂) with V(J₂) - V(J₁) = V'(ξ)(J₂ - J₁)
  have hdiff : ∀ x ∈ Set.Ioo J₁ J₂,
      HasDerivAt (fun J => valueFunction J ρ c) (valueFunctionDeriv x ρ c) x :=
    fun x hx => hasDerivAt_valueFunction (by linarith [hx.1])
  have hcont : ContinuousOn (fun J => valueFunction J ρ c) (Set.Icc J₁ J₂) := by
    apply ContinuousOn.mul
    · -- K(J) = (1-ρ)(J-1)/J is continuous for J ≠ 0
      simp only [curvatureKReal]
      apply ContinuousOn.div
      · exact continuousOn_const.mul (continuousOn_id.sub continuousOn_const)
      · exact continuousOn_id
      · intro x hx; exact ne_of_gt (show (0:ℝ) < x by linarith [hx.1])
    · -- B(J) = J^p * c is continuous for J > 0
      simp only [perCapitaBenefit]
      exact (ContinuousOn.rpow continuousOn_id continuousOn_const
        (fun x hx => Or.inl (ne_of_gt (show (0:ℝ) < x by linarith [hx.1])))).mul
        continuousOn_const
  obtain ⟨ξ, hξ_mem, hξ_eq⟩ := exists_hasDerivAt_eq_slope
    (fun J => valueFunction J ρ c) (fun x => valueFunctionDeriv x ρ c)
    (by linarith) hcont hdiff
  -- V'(ξ) > 0 since ξ > 1
  have hξ_pos : 0 < valueFunctionDeriv ξ ρ c :=
    valueFunctionDeriv_pos (by linarith [hξ_mem.1]) hρ0 hρ1 hc
  -- hξ_eq : V'(ξ) = (V(J₂) - V(J₁)) / (J₂ - J₁), so V(J₂) - V(J₁) > 0
  rw [hξ_eq] at hξ_pos
  have hVdiff : 0 < valueFunction J₂ ρ c - valueFunction J₁ ρ c := by
    rwa [div_pos_iff_of_pos_right (by linarith : (0:ℝ) < J₂ - J₁)] at hξ_pos
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Calculus.lean:112

Module Section

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

In the same file