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

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Scalar L2 representatives give integrable energy densities and finite energy bounds on every closed time interval.

  1. theorem OAI.ForcedComputation.VelocityDetector.CylinderContinuousL2.sub line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.cylinderL2_norm_sq line 24
  3. theorem OAI.ForcedComputation.VelocityDetector.CylinderContinuousL2.memLp line 33
  4. theorem OAI.ForcedComputation.VelocityDetector.CylinderContinuousL2.square_integrable line 39
  5. theorem OAI.ForcedComputation.VelocityDetector.CylinderContinuousL2.square_integral_continuous line 45
  6. theorem OAI.ForcedComputation.VelocityDetector.CylinderContinuousL2.uniform_square_integral line 51
  7. def OAI.ForcedComputation.VelocityDetector.differenceEnergy line 58
  8. def OAI.ForcedComputation.VelocityDetector.pressureDifferenceEnergy line 62
  9. theorem OAI.ForcedComputation.VelocityDetector.IsCylinderClassicalSolution.pressure_difference_integrable line 65
  10. theorem OAI.ForcedComputation.VelocityDetector.IsCylinderClassicalSolution.pressure_difference_uniform line 73
  11. theorem OAI.ForcedComputation.VelocityDetector.IsCylinderClassicalSolution.difference_square_integrable line 81
  12. theorem OAI.ForcedComputation.VelocityDetector.IsCylinderClassicalSolution.difference_energy_integrable line 92
  13. theorem OAI.ForcedComputation.VelocityDetector.IsCylinderClassicalSolution.difference_energy_continuous line 102
  14. theorem OAI.ForcedComputation.VelocityDetector.IsCylinderClassicalSolution.difference_energy_uniform line 115