OAI/MathematicalPhysics/NavierStokes/VelocityDetection/PeriodicJetsCalculus.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VelocityDetection.PeriodicSpace.Jets.init_cons line 12
  2. theorem OAI.VelocityDetection.PeriodicSpace.Jets.snoc_cons line 19
  3. def OAI.VelocityDetection.PeriodicSpace.Jets.differentiate line 30
  4. theorem OAI.VelocityDetection.PeriodicSpace.Jets.differentiate_entry line 42
  5. theorem OAI.VelocityDetection.PeriodicSpace.Jets.value_differentiate line 46
  6. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_differentiate_le line 54
  7. def OAI.VelocityDetection.PeriodicSpace.Jets.differentiateL line 61
  8. def OAI.VelocityDetection.PeriodicSpace.Jets.glueData line 69
  9. def OAI.VelocityDetection.PeriodicSpace.Jets.firstGradient line 74
  10. def OAI.VelocityDetection.PeriodicSpace.Jets.glue line 77
  11. theorem OAI.VelocityDetection.PeriodicSpace.Jets.glue_value line 107
  12. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_glue_le line 111
  13. theorem OAI.VelocityDetection.PeriodicSpace.Jets.value_add line 131
  14. theorem OAI.VelocityDetection.PeriodicSpace.Jets.value_smul line 134
  15. def OAI.VelocityDetection.PeriodicSpace.Jets.ofValue line 137
  16. theorem OAI.VelocityDetection.PeriodicSpace.Jets.value_ofValue line 140
  17. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_ofValue_le line 143
  18. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_entry_le line 149
  19. theorem OAI.VelocityDetection.PeriodicSpace.Jets.hasFDerivAt_value line 152
  20. theorem OAI.VelocityDetection.PeriodicSpace.Jets.exists_product line 170
  21. def OAI.VelocityDetection.PeriodicSpace.Jets.product line 231
  22. theorem OAI.VelocityDetection.PeriodicSpace.Jets.value_product line 234
  23. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_product_le line 237
  24. def OAI.VelocityDetection.PeriodicSpace.Jets.productLinear line 240
  25. def OAI.VelocityDetection.PeriodicSpace.Jets.productL line 266
  26. theorem OAI.VelocityDetection.PeriodicSpace.Jets.productL_apply line 270
  27. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_productL_le line 273
  28. theorem OAI.VelocityDetection.PeriodicSpace.Jets.convolve_rescale line 289
  29. def OAI.VelocityDetection.PeriodicSpace.Jets.heat line 301
  30. theorem OAI.VelocityDetection.PeriodicSpace.Jets.heat_zero line 304
  31. theorem OAI.VelocityDetection.PeriodicSpace.Jets.heat_eq_convolve line 307
  32. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_heat_le line 316
  33. theorem OAI.VelocityDetection.PeriodicSpace.Jets.continuous_heat line 320
  34. theorem OAI.VelocityDetection.PeriodicSpace.Jets.value_heat line 325
  35. def OAI.VelocityDetection.PeriodicSpace.Jets.heatDerivative line 340
  36. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_heatDerivative_le line 344
  37. theorem OAI.VelocityDetection.PeriodicSpace.Jets.continuous_average_joint line 351
  38. theorem OAI.VelocityDetection.PeriodicSpace.Jets.heatDerivative_eq_average line 362
  39. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_value_le line 384
  40. theorem OAI.VelocityDetection.PeriodicSpace.Jets.hasDerivAt_of_values line 389
  41. def OAI.VelocityDetection.PeriodicSpace.Jets.directional line 410
  42. theorem OAI.VelocityDetection.PeriodicSpace.Jets.value_directional line 413
  43. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_directional_le line 420
  44. theorem OAI.VelocityDetection.PeriodicSpace.Jets.continuous_directional line 431