OAI/Geometry/IsometricImmersion/Energy/ActualRemainderL2.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.HighEquation.chainProductL2Budget line 12
  2. def OAI.SmoothLocal.HighEquation.chainWordL2Budget line 15
  3. def OAI.SmoothLocal.HighEquation.chainSumL2Budget line 19
  4. def OAI.SmoothLocal.HighEquation.firstJetPairL2Budget line 23
  5. def OAI.SmoothLocal.HighEquation.actualHighRemainderL2Budget line 26
  6. theorem OAI.SmoothLocal.HighEquation.enorm_pow_mono_of_one_le line 31
  7. theorem OAI.SmoothLocal.HighEquation.chainProductL2Budget_lt_top line 37
  8. theorem OAI.SmoothLocal.HighEquation.chainWordL2Budget_lt_top line 44
  9. theorem OAI.SmoothLocal.HighEquation.chainSumL2Budget_lt_top line 51
  10. theorem OAI.SmoothLocal.HighEquation.actualHighRemainderL2Budget_lt_top line 59
  11. theorem OAI.SmoothLocal.HighEquation.scalar_coefficient_eLpNorm_two line 66
  12. theorem OAI.SmoothLocal.HighEquation.scalar_coefficient_eLpNorm_two_of_aestronglyMeasurable line 79
  13. theorem OAI.SmoothLocal.HighEquation.bounded_real_eLpNorm_two line 98
  14. theorem OAI.SmoothLocal.HighEquation.bounded_real_eLpNorm_two_of_aestronglyMeasurable line 110
  15. theorem OAI.SmoothLocal.HighEquation.coordinateChainFactor_memLp_two line 120
  16. theorem OAI.SmoothLocal.HighEquation.residual_product_eLpNorm_two line 145
  17. theorem OAI.SmoothLocal.HighEquation.coordinateChainTerm_eLpNorm_two line 212
  18. theorem OAI.SmoothLocal.HighEquation.coordinateChainSum_eLpNorm_two line 245
  19. theorem OAI.SmoothLocal.HighEquation.firstJetPairRemainder_continuousOn line 274
  20. theorem OAI.SmoothLocal.HighEquation.coordinateChainSum_memLp_two line 283
  21. theorem OAI.SmoothLocal.HighEquation.firstJetPairRemainder_eLpNorm_two line 299
  22. theorem OAI.SmoothLocal.HighEquation.actualHighRemainder_continuousOn line 327
  23. theorem OAI.SmoothLocal.HighEquation.actualHighRemainder_eLpNorm_two line 334
  24. theorem OAI.SmoothLocal.HighEquation.actualHighRemainder_memLp_two line 360