Documentation

Lean 4 Proof

theorem fold_underentry {J_fold ρ c cost : ℝ}
    (hJ : 1 < J_fold) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hc : 0 < c)
    (hfold : valueFunction J_fold ρ c = cost) :
    cost < valueFunction J_fold ρ c + J_fold * valueFunctionDeriv J_fold ρ c :=
  underentry_at_private_optimum hJ hρ0 hρ1 hc hfold

Dependency Graph

Location

thesis/CESProofs/Dynamics/RegimeShift.lean:47

Module Section

Paper 3c, Section 3: First-Order Regime Shift

In the same file