Documentation

Lean 4 Proof

theorem network_persistence_buffer {J_low J_high ρ c cost : ℝ}
    (hJl : 1 < J_low) (hJlh : J_low < J_high)
    (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hc : 0 < c)
    (hcost : cost ≤ valueFunction J_low ρ c) :
    cost < valueFunction J_high ρ c := by
  have hV := valueFunction_increasing hJl hJlh hρ0 hρ1 hc
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/RegimeShift.lean:87

Module Section

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

In the same file