Documentation

Lean 4 Proof

theorem self_reinforcing_entry {J₁ J₂ ρ c cost : ℝ}
    (hJ₁ : 1 < J₁) (hJ₁₂ : J₁ < J₂) (hρ0 : 0 < ρ) (hρ1 : ρ < 1)
    (hc : 0 < c) (hprofit : cost < valueFunction J₁ ρ c) :
    cost < valueFunction J₂ ρ c := by
  have hV := valueFunction_increasing hJ₁ hJ₁₂ hρ0 hρ1 hc
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:194

Module Section

## Entry-Exit Dynamics

In the same file