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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The concrete concentration cutoffs retain their mass when the radius doubles, and place that mass on the required side of the fixed observer.

  1. theorem OAI.ForcedComputation.ExpandingDetector.concentrationCutoff_le_doubled line 13
  2. theorem OAI.ForcedComputation.ExpandingDetector.concentrationCutoff_integrable line 26
  3. theorem OAI.ForcedComputation.ExpandingDetector.concentration_mass_le_doubled line 33
  4. theorem OAI.ForcedComputation.ExpandingDetector.concentrationCutoff_zero_on_upper line 42
  5. theorem OAI.ForcedComputation.ExpandingDetector.concentrationCutoff_zero_off_upper line 50
  6. theorem OAI.ForcedComputation.ExpandingDetector.concentration_nonterminal_observer line 58
  7. theorem OAI.ForcedComputation.ExpandingDetector.concentration_terminal_observer line 66