OAI/MathematicalPhysics/NavierStokes/VelocityDetection/PeriodicMildPeriodicData.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VelocityDetection.PeriodicMild.PeriodicData line 12
  2. def OAI.VelocityDetection.PeriodicMild.PeriodicData.jets line 26
  3. theorem OAI.VelocityDetection.PeriodicMild.PeriodicData.jets_value line 29
  4. theorem OAI.VelocityDetection.PeriodicMild.PeriodicData.continuous_jets line 32
  5. theorem OAI.VelocityDetection.PeriodicMild.PeriodicData.restrict_jets line 35
  6. def OAI.VelocityDetection.PeriodicMild.PeriodicData.curve line 39
  7. theorem OAI.VelocityDetection.PeriodicMild.PeriodicData.curve_apply line 42
  8. theorem OAI.VelocityDetection.PeriodicMild.PeriodicData.lower_curve line 45
  9. theorem OAI.VelocityDetection.PeriodicMild.PeriodicData.short_curve line 51
  10. def OAI.VelocityDetection.PeriodicMild.finiteSolution line 64
  11. theorem OAI.VelocityDetection.PeriodicMild.lower_finiteSolution line 67
  12. theorem OAI.VelocityDetection.PeriodicMild.short_finiteSolution line 71
  13. theorem OAI.VelocityDetection.PeriodicMild.finiteSolution_agree line 77
  14. def OAI.VelocityDetection.PeriodicMild.globalJets line 88
  15. theorem OAI.VelocityDetection.PeriodicMild.globalJets_eq_finite line 92
  16. theorem OAI.VelocityDetection.PeriodicMild.restrict_globalJets line 100
  17. theorem OAI.VelocityDetection.PeriodicMild.continuousOn_globalJets line 105
  18. def OAI.VelocityDetection.PeriodicMild.scalar line 121
  19. theorem OAI.VelocityDetection.PeriodicMild.value_globalJets line 123
  20. theorem OAI.VelocityDetection.PeriodicMild.contDiff_scalar_space line 128