OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TailSpaceIntegrableCompatible.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VelocityDetection.TailSpace.integrable_compatible line 16
  2. theorem OAI.VelocityDetection.TailSpace.norm_compatible_apply_le line 19
  3. theorem OAI.VelocityDetection.TailSpace.integrable_mul line 23
  4. def OAI.VelocityDetection.TailSpace.mul line 28
  5. theorem OAI.VelocityDetection.TailSpace.mul_apply line 33
  6. theorem OAI.VelocityDetection.TailSpace.integral_norm_eq line 36
  7. theorem OAI.VelocityDetection.TailSpace.norm_mul_le line 42
  8. def OAI.VelocityDetection.TailSpace.Jets.restrict line 77
  9. theorem OAI.VelocityDetection.TailSpace.Jets.restrict_entry line 82
  10. theorem OAI.VelocityDetection.TailSpace.Jets.restrict_value line 86
  11. theorem OAI.VelocityDetection.TailSpace.Jets.norm_restrict_le line 89
  12. def OAI.VelocityDetection.TailSpace.Jets.restrictL line 96
  13. theorem OAI.VelocityDetection.TailSpace.Jets.init_cons line 103
  14. theorem OAI.VelocityDetection.TailSpace.Jets.snoc_cons line 110
  15. def OAI.VelocityDetection.TailSpace.Jets.differentiate line 121
  16. theorem OAI.VelocityDetection.TailSpace.Jets.differentiate_entry line 133
  17. theorem OAI.VelocityDetection.TailSpace.Jets.value_differentiate line 137
  18. theorem OAI.VelocityDetection.TailSpace.Jets.norm_differentiate_le line 145
  19. def OAI.VelocityDetection.TailSpace.Jets.differentiateL line 152
  20. def OAI.VelocityDetection.TailSpace.Jets.glueData line 160
  21. def OAI.VelocityDetection.TailSpace.Jets.firstGradient line 165
  22. def OAI.VelocityDetection.TailSpace.Jets.glue line 168
  23. theorem OAI.VelocityDetection.TailSpace.Jets.glue_value line 198
  24. theorem OAI.VelocityDetection.TailSpace.Jets.norm_glue_le line 202
  25. theorem OAI.VelocityDetection.TailSpace.Jets.value_add line 227
  26. theorem OAI.VelocityDetection.TailSpace.Jets.value_smul line 230
  27. def OAI.VelocityDetection.TailSpace.Jets.ofValue line 233
  28. theorem OAI.VelocityDetection.TailSpace.Jets.value_ofValue line 236
  29. theorem OAI.VelocityDetection.TailSpace.Jets.norm_ofValue_le line 239
  30. theorem OAI.VelocityDetection.TailSpace.Jets.norm_entry_le line 245
  31. theorem OAI.VelocityDetection.TailSpace.Jets.hasFDerivAt_value line 248
  32. theorem OAI.VelocityDetection.TailSpace.Jets.exists_product line 266
  33. def OAI.VelocityDetection.TailSpace.Jets.product line 327
  34. theorem OAI.VelocityDetection.TailSpace.Jets.value_product line 330
  35. theorem OAI.VelocityDetection.TailSpace.Jets.norm_product_le line 333
  36. def OAI.VelocityDetection.TailSpace.Jets.productLinear line 336
  37. def OAI.VelocityDetection.TailSpace.Jets.productL line 362
  38. theorem OAI.VelocityDetection.TailSpace.Jets.productL_apply line 366
  39. theorem OAI.VelocityDetection.TailSpace.Jets.norm_productL_le line 369
  40. def OAI.VelocityDetection.TailSpace.Jets.heatGradient line 390
  41. theorem OAI.VelocityDetection.TailSpace.Jets.heatGradient_eq line 395
  42. theorem OAI.VelocityDetection.TailSpace.Jets.norm_heatGradient_le line 400
  43. theorem OAI.VelocityDetection.TailSpace.Jets.continuous_heat_joint line 407
  44. theorem OAI.VelocityDetection.TailSpace.Jets.continuousOn_heatGradient_joint line 412