Documentation

Lean 4 Proof

theorem entry_driven_by_value_function {J ρ c cost : ℝ}
    (hcost : cost < valueFunction J ρ c) :
    0 < valueFunction J ρ c - cost := by
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:184

Module Section

## Entry-Exit Dynamics

In the same file