OAI/Geometry/IsometricImmersion/Darboux/QResidualL2.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.HighEquation.qWordSliceBudget line 13
  2. def OAI.SmoothLocal.HighEquation.qChainSliceBudget line 17
  3. def OAI.SmoothLocal.HighEquation.qPairSliceBudget line 21
  4. def OAI.SmoothLocal.HighEquation.qRemainderSliceBudget line 24
  5. theorem OAI.SmoothLocal.HighEquation.qWordSliceBudget_lt_top line 29
  6. theorem OAI.SmoothLocal.HighEquation.qChainSliceBudget_lt_top line 35
  7. theorem OAI.SmoothLocal.HighEquation.qRemainderSliceBudget_lt_top line 42
  8. theorem OAI.SmoothLocal.HighEquation.qCoordinateScalarTerm_continuousOn line 50
  9. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainTerm_continuousOn line 60
  10. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainSum_continuousOn line 71
  11. theorem OAI.SmoothLocal.HighEquation.q_residual_product_eLpNorm_two line 79
  12. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainTerm_slice_eLpNorm_two line 147
  13. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainSum_slice_eLpNorm_two line 177
  14. theorem OAI.SmoothLocal.HighEquation.qFirstJetPairRemainder_continuousOn line 204
  15. theorem OAI.SmoothLocal.HighEquation.qFirstJetPairRemainder_slice_eLpNorm_two line 212
  16. theorem OAI.SmoothLocal.HighEquation.actualQHighRemainder_continuousOn line 244
  17. theorem OAI.SmoothLocal.HighEquation.actualQHighRemainder_slice_memLp_two line 251
  18. theorem OAI.SmoothLocal.HighEquation.actualQHighRemainder_slice_eLpNorm_two line 259