OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TailJets.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VelocityDetection.TailSpace.Jets.Index line 16
  2. abbrev OAI.VelocityDetection.TailSpace.Jets.Data line 18
  3. def OAI.VelocityDetection.TailSpace.Jets.gradient line 20
  4. theorem OAI.VelocityDetection.TailSpace.Jets.gradient_zero line 24
  5. theorem OAI.VelocityDetection.TailSpace.Jets.gradient_add line 28
  6. theorem OAI.VelocityDetection.TailSpace.Jets.gradient_smul line 33
  7. def OAI.VelocityDetection.TailSpace.Jets.compatibleJets line 38
  8. theorem OAI.VelocityDetection.TailSpace.Jets.gradient_sub line 53
  9. theorem OAI.VelocityDetection.TailSpace.Jets.norm_gradient_le line 65
  10. theorem OAI.VelocityDetection.TailSpace.Jets.gradient_tendstoUniformly line 85
  11. theorem OAI.VelocityDetection.TailSpace.Jets.component_tendstoUniformly line 103
  12. theorem OAI.VelocityDetection.TailSpace.Jets.compatibleJets_closed line 110
  13. instance OAI.VelocityDetection.TailSpace.Jets.(instance at line 117) line 117
  14. def OAI.VelocityDetection.TailSpace.Jets.entry line 120
  15. def OAI.VelocityDetection.TailSpace.Jets.value line 123
  16. def OAI.VelocityDetection.TailSpace.Jets.wordPartial line 126
  17. theorem OAI.VelocityDetection.TailSpace.Jets.wordPartial_nil line 130
  18. theorem OAI.VelocityDetection.TailSpace.Jets.wordPartial_cons line 133
  19. theorem OAI.VelocityDetection.TailSpace.Jets.entry_hasFDerivAt line 137
  20. theorem OAI.VelocityDetection.TailSpace.Jets.entry_partialD line 142
  21. theorem OAI.VelocityDetection.TailSpace.Jets.entry_eq_wordPartial line 152
  22. theorem OAI.VelocityDetection.TailSpace.Jets.contDiff_entry line 167
  23. theorem OAI.VelocityDetection.TailSpace.Jets.contDiff_value line 183
  24. theorem OAI.VelocityDetection.TailSpace.Jets.compatible_ext line 186
  25. theorem OAI.VelocityDetection.TailSpace.Jets.value_injective line 195
  26. theorem OAI.VelocityDetection.TailSpace.Jets.derivative_tails line 205
  27. def OAI.VelocityDetection.TailSpace.translate line 226
  28. theorem OAI.VelocityDetection.TailSpace.translate_apply line 232
  29. theorem OAI.VelocityDetection.TailSpace.translate_zero line 235
  30. theorem OAI.VelocityDetection.TailSpace.translate_add line 240
  31. theorem OAI.VelocityDetection.TailSpace.norm_translate_le line 246
  32. theorem OAI.VelocityDetection.TailSpace.norm_translate line 258
  33. def OAI.VelocityDetection.TailSpace.translateLI line 265
  34. theorem OAI.VelocityDetection.TailSpace.continuous_translate_C0 line 279
  35. theorem OAI.VelocityDetection.TailSpace.continuous_translate line 292
  36. instance OAI.VelocityDetection.TailSpace.Jets.(instance at line 316) line 316
  37. instance OAI.VelocityDetection.TailSpace.Jets.(instance at line 319) line 319
  38. def OAI.VelocityDetection.TailSpace.Jets.translate line 322
  39. theorem OAI.VelocityDetection.TailSpace.Jets.translate_entry line 329
  40. theorem OAI.VelocityDetection.TailSpace.Jets.translate_value line 333
  41. theorem OAI.VelocityDetection.TailSpace.Jets.translate_zero line 336
  42. theorem OAI.VelocityDetection.TailSpace.Jets.translate_add line 341
  43. theorem OAI.VelocityDetection.TailSpace.Jets.norm_translate line 347
  44. def OAI.VelocityDetection.TailSpace.Jets.translateLI line 352
  45. theorem OAI.VelocityDetection.TailSpace.Jets.continuous_translate line 364
  46. def OAI.VelocityDetection.TailSpace.Jets.evaluate line 384
  47. theorem OAI.VelocityDetection.TailSpace.Jets.evaluate_apply line 398
  48. theorem OAI.VelocityDetection.TailSpace.Jets.integrable_average line 401
  49. def OAI.VelocityDetection.TailSpace.Jets.average line 416
  50. theorem OAI.VelocityDetection.TailSpace.Jets.norm_average_le line 419
  51. theorem OAI.VelocityDetection.TailSpace.Jets.value_average line 428