OAI/MathematicalPhysics/NavierStokes/VelocityDetection/MildScalar.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VelocityDetection.MildScalar.E line 19
  2. abbrev OAI.VelocityDetection.MildScalar.TimeCurve line 21
  3. def OAI.VelocityDetection.MildScalar.driftKernel line 40
  4. theorem OAI.VelocityDetection.MildScalar.driftKernel_apply line 43
  5. theorem OAI.VelocityDetection.MildScalar.continuousOn_driftKernel line 50
  6. def OAI.VelocityDetection.MildScalar.driftConstant line 66
  7. def OAI.VelocityDetection.MildScalar.driftBound line 69
  8. theorem OAI.VelocityDetection.MildScalar.driftConstant_nonneg line 71
  9. theorem OAI.VelocityDetection.MildScalar.driftBound_nonneg line 76
  10. theorem OAI.VelocityDetection.MildScalar.integrableOn_driftBound line 81
  11. theorem OAI.VelocityDetection.MildScalar.norm_driftKernel_le line 86
  12. def OAI.VelocityDetection.MildScalar.sourceKernel line 110
  13. theorem OAI.VelocityDetection.MildScalar.continuous_sourceKernel line 112
  14. def OAI.VelocityDetection.MildScalar.sourceCurve line 120
  15. theorem OAI.VelocityDetection.MildScalar.sourceCurve_apply line 125
  16. theorem OAI.VelocityDetection.MildScalar.existsUnique_mild line 132