OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/PeriodizeBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Periodization preserves a sup bound when the support is shorter than one period: at any point, at most one translated copy contributes.

  1. theorem OAI.ForcedComputation.VelocityDetector.iteratedDeriv_support_interval line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.iteratedDeriv_smooth line 23
  3. theorem OAI.ForcedComputation.VelocityDetector.periodize_iteratedDeriv line 31
  4. theorem OAI.ForcedComputation.VelocityDetector.periodize_unit_bound line 41