Documentation

Lean 4 Proof

theorem trivial_fixed_point (lambda mu : ℝ) {cost : ℝ} (hcost : 0 ≤ cost) :
    netEntryFlow lambda mu 0 cost 0 = 0 := by
  simp only [netEntryFlow, entryRate, exitRate, mul_zero, sub_zero]
  simp only [max_eq_left (show 0 - cost ≤ 0 by linarith), mul_zero]

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:168

Module Section

## Entry-Exit Dynamics

In the same file