OAI/Geometry/IsometricImmersion/Energy/MixedRemainderL2.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.HighEquation.mixedRemainderL2Budget line 12
2. theorem OAI.SmoothLocal.HighEquation.mixedRemainderL2Budget_lt_top line 16
3. theorem OAI.SmoothLocal.HighEquation.mixedFaaRemainder_continuousOn line 25
4. theorem OAI.SmoothLocal.HighEquation.mixed_product_eLpNorm_two line 38
5. theorem OAI.SmoothLocal.HighEquation.mixedFaaTerm_eLpNorm_two line 93
6. theorem OAI.SmoothLocal.HighEquation.mixedFaaRemainder_eLpNorm_two line 133
7. theorem OAI.SmoothLocal.HighEquation.mixedFaaRemainder_memLp_two line 184