OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/ExpandingRetainedObservation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The concrete half-plane observation follows from the proved retained mass bound and the terminal flag of the actual recorder configuration.

  1. def OAI.ForcedComputation.ExpandingDetector.accumulatedLoss line 14
  2. theorem OAI.ForcedComputation.ExpandingDetector.accumulatedLoss_lt line 18
  3. theorem OAI.ForcedComputation.ExpandingDetector.configurationCenter_terminal line 23
  4. theorem OAI.ForcedComputation.ExpandingDetector.configurationCenter_nonterminal line 30
  5. theorem OAI.ForcedComputation.ExpandingDetector.retained_terminal_observation line 38
  6. theorem OAI.ForcedComputation.ExpandingDetector.accumulatedLoss_partial_le line 60
  7. theorem OAI.ForcedComputation.ExpandingDetector.initialLoss_partial_le line 74