OAI/MathematicalPhysics/NavierStokes/VelocityDetection/PeriodicMild.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VelocityDetection.PeriodicMild.E line 14
  2. abbrev OAI.VelocityDetection.PeriodicMild.TimeCurve line 16
  3. def OAI.VelocityDetection.PeriodicMild.driftKernel line 30
  4. theorem OAI.VelocityDetection.PeriodicMild.driftKernel_apply line 33
  5. theorem OAI.VelocityDetection.PeriodicMild.continuousOn_driftKernel line 40
  6. def OAI.VelocityDetection.PeriodicMild.driftConstant line 56
  7. def OAI.VelocityDetection.PeriodicMild.driftBound line 59
  8. theorem OAI.VelocityDetection.PeriodicMild.driftConstant_nonneg line 61
  9. theorem OAI.VelocityDetection.PeriodicMild.driftBound_nonneg line 66
  10. theorem OAI.VelocityDetection.PeriodicMild.integrableOn_driftBound line 71
  11. theorem OAI.VelocityDetection.PeriodicMild.norm_driftKernel_le line 76
  12. def OAI.VelocityDetection.PeriodicMild.sourceKernel line 100
  13. theorem OAI.VelocityDetection.PeriodicMild.continuous_sourceKernel line 102
  14. def OAI.VelocityDetection.PeriodicMild.sourceCurve line 110
  15. theorem OAI.VelocityDetection.PeriodicMild.sourceCurve_apply line 115
  16. theorem OAI.VelocityDetection.PeriodicMild.existsUnique_mild line 122