OAI/Analysis/LipschitzHilbert/Estimates/TerminalFlow.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Conservation and good-terminal domination for finite stopped path flows.

  1. structure OAI.LipschitzHilbert.TerminalFlow line 17

    Source documentation

    A finite path flow with a unique final edge for each terminal top. The balance law includes both continuing and terminating mass.

    structure TerminalFlow (N : ℕ) where
…
  2. def OAI.LipschitzHilbert.TerminalFlow.terminalProbability line 38
  3. theorem OAI.LipschitzHilbert.TerminalFlow.terminalProbability_nonnegative line 41
  4. theorem OAI.LipschitzHilbert.TerminalFlow.exiting_nonnegative line 44
  5. theorem OAI.LipschitzHilbert.TerminalFlow.occupancy_total_le_one line 52
  6. theorem OAI.LipschitzHilbert.TerminalFlow.occupancy_le_one line 63
  7. theorem OAI.LipschitzHilbert.TerminalFlow.terminalProbability_le_rate line 67
  8. theorem OAI.LipschitzHilbert.TerminalFlow.terminalProbability_total line 71
  9. theorem OAI.LipschitzHilbert.TerminalFlow.bad_terminal_probability_le line 98
  10. theorem OAI.LipschitzHilbert.TerminalFlow.good_terminal_probability_half line 104