Documentation

Lean 4 Proof

theorem phase_portrait (lambda mu cost : ℝ)
    (hlam : 0 < lambda) (hmu : 0 < mu) (hcost : 0 < cost) :
    -- Three fixed points: J=0, J_crit, J_high
    -- J=0 stable, J_crit unstable, J_high stable
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:160

Module Section

## Entry-Exit Dynamics

In the same file