OAI/Geometry/IsometricImmersion/Estimates/MixedRemainderFactors.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.HighEquation.fullJet_fixed_input_continuousOn line 13
2. theorem OAI.SmoothLocal.HighEquation.mixedFaaFactor_continuousOn line 25
3. theorem OAI.SmoothLocal.HighEquation.mixedFaaTerm_continuousOn line 33
4. theorem OAI.SmoothLocal.HighEquation.fullJet_coordinate_projection_abs_le_one line 48
5. theorem OAI.SmoothLocal.HighEquation.mixedBlock_spatial_abs_le_one line 61
6. theorem OAI.SmoothLocal.HighEquation.mixed_high_factor_unique line 74
7. theorem OAI.SmoothLocal.HighEquation.mixedBlock_low_norm_bound line 84
8. theorem OAI.SmoothLocal.HighEquation.mixedBlock_high_eLpNorm_bound line 111
9. theorem OAI.SmoothLocal.HighEquation.heightPFirst_abs_le_fullP_one line 144