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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The limiting step in the noncompact energy argument. A vanishing boundary error is allowed in each compactly localized energy estimate.

  1. theorem OAI.ForcedComputation.VelocityDetector.localized_energy_bound line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.zero_of_localized_energy_limit line 55