OAI/MathematicalPhysics/NavierStokes/VelocityDetection/PeriodicJets.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VelocityDetection.PeriodicSpace.Jets.Index line 12
  2. abbrev OAI.VelocityDetection.PeriodicSpace.Jets.Data line 14
  3. def OAI.VelocityDetection.PeriodicSpace.Jets.gradient line 16
  4. theorem OAI.VelocityDetection.PeriodicSpace.Jets.gradient_zero line 20
  5. theorem OAI.VelocityDetection.PeriodicSpace.Jets.gradient_add line 24
  6. theorem OAI.VelocityDetection.PeriodicSpace.Jets.gradient_smul line 29
  7. def OAI.VelocityDetection.PeriodicSpace.Jets.compatibleJets line 34
  8. theorem OAI.VelocityDetection.PeriodicSpace.Jets.gradient_sub line 49
  9. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_gradient_le line 60
  10. theorem OAI.VelocityDetection.PeriodicSpace.Jets.gradient_tendstoUniformly line 80
  11. theorem OAI.VelocityDetection.PeriodicSpace.Jets.component_tendstoUniformly line 98
  12. theorem OAI.VelocityDetection.PeriodicSpace.Jets.compatibleJets_closed line 105
  13. instance OAI.VelocityDetection.PeriodicSpace.Jets.(instance at line 112) line 112
  14. def OAI.VelocityDetection.PeriodicSpace.Jets.entry line 115
  15. def OAI.VelocityDetection.PeriodicSpace.Jets.value line 118
  16. def OAI.VelocityDetection.PeriodicSpace.Jets.wordPartial line 121
  17. theorem OAI.VelocityDetection.PeriodicSpace.Jets.wordPartial_nil line 125
  18. theorem OAI.VelocityDetection.PeriodicSpace.Jets.wordPartial_cons line 128
  19. theorem OAI.VelocityDetection.PeriodicSpace.Jets.entry_hasFDerivAt line 132
  20. theorem OAI.VelocityDetection.PeriodicSpace.Jets.entry_partialD line 137
  21. theorem OAI.VelocityDetection.PeriodicSpace.Jets.entry_eq_wordPartial line 147
  22. theorem OAI.VelocityDetection.PeriodicSpace.Jets.contDiff_entry line 162
  23. theorem OAI.VelocityDetection.PeriodicSpace.Jets.contDiff_value line 178
  24. theorem OAI.VelocityDetection.PeriodicSpace.Jets.compatible_ext line 181
  25. theorem OAI.VelocityDetection.PeriodicSpace.Jets.value_injective line 184
  26. instance OAI.VelocityDetection.PeriodicSpace.Jets.(instance at line 194) line 194
  27. instance OAI.VelocityDetection.PeriodicSpace.Jets.(instance at line 197) line 197
  28. def OAI.VelocityDetection.PeriodicSpace.Jets.translate line 200
  29. theorem OAI.VelocityDetection.PeriodicSpace.Jets.translate_entry line 207
  30. theorem OAI.VelocityDetection.PeriodicSpace.Jets.translate_value line 211
  31. theorem OAI.VelocityDetection.PeriodicSpace.Jets.translate_zero line 214
  32. theorem OAI.VelocityDetection.PeriodicSpace.Jets.translate_add line 219
  33. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_translate line 225
  34. def OAI.VelocityDetection.PeriodicSpace.Jets.translateLI line 230
  35. theorem OAI.VelocityDetection.PeriodicSpace.Jets.continuous_translate line 242
  36. def OAI.VelocityDetection.PeriodicSpace.Jets.evaluate line 258
  37. theorem OAI.VelocityDetection.PeriodicSpace.Jets.evaluate_apply line 271
  38. theorem OAI.VelocityDetection.PeriodicSpace.Jets.integrable_average line 274
  39. def OAI.VelocityDetection.PeriodicSpace.Jets.average line 289
  40. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_average_le line 292
  41. theorem OAI.VelocityDetection.PeriodicSpace.Jets.value_average line 301
  42. def OAI.VelocityDetection.PeriodicSpace.Jets.averageL line 307
  43. theorem OAI.VelocityDetection.PeriodicSpace.Jets.averageL_apply line 325
  44. def OAI.VelocityDetection.PeriodicSpace.Jets.convolve line 328
  45. theorem OAI.VelocityDetection.PeriodicSpace.Jets.value_convolve line 331
  46. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_convolve_le line 336
  47. theorem OAI.VelocityDetection.PeriodicSpace.Jets.continuous_average line 340
  48. theorem OAI.VelocityDetection.PeriodicSpace.Jets.average_zero_scale line 355
  49. theorem OAI.VelocityDetection.PeriodicSpace.Jets.average_tendsto_identity line 359
  50. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_average_le_of_probability_kernel line 365
  51. theorem OAI.VelocityDetection.PeriodicSpace.norm_compatible_apply_le line 380
  52. def OAI.VelocityDetection.PeriodicSpace.mul line 383
  53. theorem OAI.VelocityDetection.PeriodicSpace.mul_apply line 385
  54. theorem OAI.VelocityDetection.PeriodicSpace.norm_mul_le line 388
  55. def OAI.VelocityDetection.PeriodicSpace.Jets.restrict line 400
  56. theorem OAI.VelocityDetection.PeriodicSpace.Jets.restrict_entry line 405
  57. theorem OAI.VelocityDetection.PeriodicSpace.Jets.restrict_value line 409
  58. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_restrict_le line 412
  59. def OAI.VelocityDetection.PeriodicSpace.Jets.restrictL line 419