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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sufficiently large compact tests are identically one on the common support of the finite-time drift and source.

  1. theorem OAI.ForcedComputation.VelocityDetector.CompactPlaneCoefficients.cutoff_eventually_exact line 14