OAI/MathematicalPhysics/NavierStokes/VelocityDetection/PeriodicSpaceRestrictRestrict.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VelocityDetection.PeriodicSpace.Jets.restrict_restrict line 16
  2. theorem OAI.VelocityDetection.PeriodicSpace.Jets.restrict_differentiate line 21
  3. theorem OAI.VelocityDetection.PeriodicSpace.Jets.heatGradient_restrict line 28
  4. theorem OAI.VelocityDetection.PeriodicSpace.Jets.normal_translate_directional line 38
  5. def OAI.VelocityDetection.PeriodicSpace.Jets.normalAverageDerivative line 51
  6. theorem OAI.VelocityDetection.PeriodicSpace.Jets.normalAverageDerivative_integrable line 55
  7. theorem OAI.VelocityDetection.PeriodicSpace.Jets.norm_normalAverageDerivative line 60
  8. theorem OAI.VelocityDetection.PeriodicSpace.Jets.hasDerivAt_normal_integrand line 73
  9. theorem OAI.VelocityDetection.PeriodicSpace.Jets.hasDerivAt_average_normal line 82
  10. def OAI.VelocityDetection.PeriodicSpace.Jets.laplaceJet line 103
  11. def OAI.VelocityDetection.PeriodicSpace.Jets.laplaceL line 106
  12. theorem OAI.VelocityDetection.PeriodicSpace.Jets.laplaceL_apply line 109
  13. theorem OAI.VelocityDetection.PeriodicSpace.Jets.value_laplaceJet line 112
  14. theorem OAI.VelocityDetection.PeriodicSpace.Jets.hasDerivAt_average_normal_laplace line 118
  15. theorem OAI.VelocityDetection.PeriodicSpace.Jets.hasDerivAt_heat line 136
  16. theorem OAI.VelocityDetection.PeriodicSpace.Jets.hasDerivWithinAt_heat_zero line 157
  17. def OAI.VelocityDetection.PeriodicSpace.Jets.heatExtension line 187
  18. theorem OAI.VelocityDetection.PeriodicSpace.Jets.heatExtension_of_nonneg line 190
  19. theorem OAI.VelocityDetection.PeriodicSpace.Jets.heat_of_nonpos line 195
  20. theorem OAI.VelocityDetection.PeriodicSpace.Jets.heatExtension_of_nonpos line 200
  21. theorem OAI.VelocityDetection.PeriodicSpace.Jets.continuous_heatExtension line 205
  22. theorem OAI.VelocityDetection.PeriodicSpace.Jets.continuous_heatExtension_derivative line 220
  23. theorem OAI.VelocityDetection.PeriodicSpace.Jets.hasDerivAt_heatExtension line 228
  24. def OAI.VelocityDetection.PeriodicSpace.Jets.duhamel line 261
  25. def OAI.VelocityDetection.PeriodicSpace.Jets.extendedDuhamel line 264
  26. theorem OAI.VelocityDetection.PeriodicSpace.Jets.extendedDuhamel_eq line 267
  27. theorem OAI.VelocityDetection.PeriodicSpace.Jets.hasDerivAt_extendedDuhamel line 274
  28. theorem OAI.VelocityDetection.PeriodicSpace.Jets.hasDerivWithinAt_duhamel line 294
  29. theorem OAI.VelocityDetection.PeriodicSpace.Jets.differentiateL_apply line 311
  30. theorem OAI.VelocityDetection.PeriodicSpace.Jets.differentiate_translate line 314
  31. theorem OAI.VelocityDetection.PeriodicSpace.Jets.differentiate_average line 320
  32. theorem OAI.VelocityDetection.PeriodicSpace.Jets.differentiate_heat line 327
  33. theorem OAI.VelocityDetection.PeriodicSpace.Jets.laplace_heat line 332
  34. theorem OAI.VelocityDetection.PeriodicSpace.Jets.restrict_laplace line 336
  35. theorem OAI.VelocityDetection.PeriodicSpace.Jets.laplace_integral_heat line 343
  36. theorem OAI.VelocityDetection.PeriodicSpace.cover_sub line 361
  37. theorem OAI.VelocityDetection.PeriodicSpace.openQuotient_cover line 363
  38. def OAI.VelocityDetection.PeriodicSpace.ofPeriodic line 366
  39. theorem OAI.VelocityDetection.PeriodicSpace.realLift_ofPeriodic line 370
  40. theorem OAI.VelocityDetection.PeriodicSpace.periodic_partialD line 376
  41. theorem OAI.VelocityDetection.PeriodicSpace.continuous_ofPeriodic_curve line 392
  42. theorem OAI.VelocityDetection.PeriodicSpace.Jets.wordPartial_tailWordPartial line 412
  43. theorem OAI.VelocityDetection.PeriodicSpace.Jets.contDiff_wordPartial line 421
  44. theorem OAI.VelocityDetection.PeriodicSpace.Jets.contDiff_uncurry_wordPartial line 426
  45. theorem OAI.VelocityDetection.PeriodicSpace.Jets.periodic_wordPartial line 432
  46. def OAI.VelocityDetection.PeriodicSpace.Jets.ofSmoothPeriodic line 441
  47. theorem OAI.VelocityDetection.PeriodicSpace.Jets.value_ofSmoothPeriodic line 457