OAI/Geometry/IsometricImmersion/Estimates/RemainderAreaBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.HighEquation.chainProductL2Budget_mono_area line 14
2. theorem OAI.SmoothLocal.HighEquation.chainWordL2Budget_mono_area line 20
3. theorem OAI.SmoothLocal.HighEquation.chainSumL2Budget_mono_area line 27
4. theorem OAI.SmoothLocal.HighEquation.actualHighRemainderL2Budget_mono_area line 34
5. theorem OAI.SmoothLocal.HighEquation.mixedRemainderL2Budget_mono_area line 39
6. theorem OAI.SmoothLocal.HighEquation.mixedXBudget_mono_remainder line 47
7. def OAI.SmoothLocal.HighEquation.uniformMixedOrderBudget line 53
8. theorem OAI.SmoothLocal.HighEquation.uniformMixedOrderBudget_coe line 56
9. theorem OAI.SmoothLocal.HighEquation.coordinateL2Bound_order_step line 64