OAI/MathematicalPhysics/NavierStokes/VelocityDetection/MildScalarGlobalJetsClamp.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.VelocityDetection.MildScalar.globalJets_clamp line 19
2. theorem OAI.VelocityDetection.MildScalar.continuous_globalJets line 25
3. def OAI.VelocityDetection.MildScalar.pdeSource line 31
4. theorem OAI.VelocityDetection.MildScalar.continuous_pdeSource line 35
5. theorem OAI.VelocityDetection.MildScalar.restrict_pdeSource line 45
6. theorem OAI.VelocityDetection.MildScalar.drift_global line 53
7. theorem OAI.VelocityDetection.MildScalar.globalJets_mild line 68
8. theorem OAI.VelocityDetection.MildScalar.heat_sub_sum line 86
9. theorem OAI.VelocityDetection.MildScalar.combined_integrands line 93
10. theorem OAI.VelocityDetection.MildScalar.globalJets_integral line 106
11. theorem OAI.VelocityDetection.MildScalar.globalJets_integral_time line 135
12. theorem OAI.VelocityDetection.MildScalar.globalJets_zero line 144
13. theorem OAI.VelocityDetection.MildScalar.globalJets_nonpos line 147
14. theorem OAI.VelocityDetection.MildScalar.globalJets_duhamel line 151
15. def OAI.VelocityDetection.MildScalar.timeGenerator line 156
16. theorem OAI.VelocityDetection.MildScalar.continuous_timeGenerator line 159
17. theorem OAI.VelocityDetection.MildScalar.hasDerivWithinAt_globalJets line 164
18. theorem OAI.VelocityDetection.MildScalar.c1_globalJets line 177
19. def OAI.VelocityDetection.MildScalar.valueTailL line 187
20. theorem OAI.VelocityDetection.MildScalar.valueTailL_apply line 197
21. theorem OAI.VelocityDetection.MildScalar.scalar_C1Tails line 200
22. theorem OAI.VelocityDetection.MildScalar.sourceJets_nonpos line 233
23. theorem OAI.VelocityDetection.MildScalar.timeGenerator_nonpos line 238
24. theorem OAI.VelocityDetection.MildScalar.hasDerivAt_globalJets line 249
25. theorem OAI.VelocityDetection.MildScalar.contDiff_globalJets_nat line 270
26. theorem OAI.VelocityDetection.MildScalar.contDiff_globalJets line 292