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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compact horizontal localization of integrals over one vertical period. These lemmas are the measure-theoretic part of the localized energy identity.

  1. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.ae_vertical_period line 18
  2. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.integrable_horizontal_compact line 23
  3. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.slice_continuous line 33
  4. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.compact_integral_hasDerivAt line 39
  5. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.integral_restrict_eq_of_horizontal_support line 67
  6. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.supported_integral_hasDerivAt line 75