OAI/Geometry/IsometricImmersion/Energy/MovingIntervalSourceL2.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Hyperbolic.spatialProduct line 13
  2. def OAI.SmoothLocal.Hyperbolic.spatialSourceTerm line 17
  3. def OAI.SmoothLocal.Hyperbolic.spatialLowFactorBound line 21
  4. def OAI.SmoothLocal.Hyperbolic.spatialProductL2Budget line 24
  5. theorem OAI.SmoothLocal.Hyperbolic.spatialProductL2Budget_lt_top line 28
  6. theorem OAI.SmoothLocal.Hyperbolic.spatialProduct_contDiffOn line 34
  7. theorem OAI.SmoothLocal.Hyperbolic.spatialProduct_eLpNorm_two line 43
  8. theorem OAI.SmoothLocal.Hyperbolic.real_interval_coefficient_eLpNorm_two line 108
  9. theorem OAI.SmoothLocal.Hyperbolic.real_interval_coefficient_eLpNorm_two_of_aestronglyMeasurable line 122
  10. theorem OAI.SmoothLocal.Hyperbolic.spatialSourceTerm_memLp_two line 141
  11. theorem OAI.SmoothLocal.Hyperbolic.spatialSourceTerm_eLpNorm_two line 152
  12. theorem OAI.SmoothLocal.Hyperbolic.spatialSourceTerm_eLpNorm_two_of_aestronglyMeasurable line 175
  13. def OAI.SmoothLocal.Hyperbolic.spatialSourceSum line 196
  14. theorem OAI.SmoothLocal.Hyperbolic.spatialSourceSum_eLpNorm_two line 202