OAI/Geometry/Immersion/ClosedSurface/QuadraticError.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.QuadraticMean.contDiffOn_conjugate line 12
2. lemma OAI.ClosedSurfaceR4.QuadraticMean.weighted_conjugate line 18
3. def OAI.ClosedSurfaceR4.QuadraticMean.halfReCLM line 36
4. lemma OAI.ClosedSurfaceR4.QuadraticMean.halfReCLM_apply line 38
5. lemma OAI.ClosedSurfaceR4.QuadraticMean.halfReCLM_norm_le line 41
6. lemma OAI.ClosedSurfaceR4.QuadraticMean.contDiffOn_zeroPair line 49
7. lemma OAI.ClosedSurfaceR4.QuadraticMean.weighted_zeroPair line 58
8. lemma OAI.ClosedSurfaceR4.QuadraticMean.zeroPair_sub_left line 76
9. lemma OAI.ClosedSurfaceR4.QuadraticMean.zeroPair_sub_right line 80
10. lemma OAI.ClosedSurfaceR4.QuadraticMean.zeroPair_error_identity line 85
11. theorem OAI.ClosedSurfaceR4.QuadraticMean.weighted_zeroPair_error line 93