OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Scalar/PlaneCutoffLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact concentration tests tend to one on the plane, and recover the mass of every integrable scalar by dominated convergence.

  1. theorem OAI.ForcedComputation.ExpandingDetector.concentrationCutoff_eventually_one line 14
  2. theorem OAI.ForcedComputation.ExpandingDetector.concentrationCutoff_tendsto_one line 25
  3. theorem OAI.ForcedComputation.ExpandingDetector.concentrationCutoff_integral_limit line 31