Documentation

Lean 4 Proof

theorem valueFunction_pos {J ρ c : ℝ}
    (hJ : 1 < J) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hc : 0 < c) :
    0 < valueFunction J ρ c := by
  -- Find J₀ ∈ (1, J) to apply monotonicity
  -- Actually: pick J₁ = (1+J)/2, show V(J₁) > V_at_1 = 0 and V(J) > V(J₁) > 0
  -- Simpler: use that V(J) > V at some J₀ close to 1 where V > 0
  -- Simplest: direct calculation. V(J) = K(J) * B(J), both positive for J > 1
  apply mul_pos (curvatureKReal_pos hJ hρ1) (perCapitaBenefit_pos (by linarith) hc)

Dependency Graph

Location

thesis/CESProofs/EntryExit/Calculus.lean:148

Module Section

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

In the same file