OAI/Geometry/Immersion/ClosedSurface/PullbackBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.PhaseMean.weighted_base_fst line 16
2. lemma OAI.ClosedSurfaceR4.PhaseMean.weighted_base_snd line 23
3. lemma OAI.ClosedSurfaceR4.PhaseMean.weighted_complexEvaluate line 30
4. lemma OAI.ClosedSurfaceR4.PhaseMean.weighted_complexPullbackField_apply line 63
5. lemma OAI.ClosedSurfaceR4.PhaseMean.contDiffOn_complexify line 79
6. lemma OAI.ClosedSurfaceR4.PhaseMean.weighted_complexify line 85
7. lemma OAI.ClosedSurfaceR4.PhaseMean.realPart_complexify line 94
8. lemma OAI.ClosedSurfaceR4.PhaseMean.contDiffOn_pullbackField_apply line 97
9. lemma OAI.ClosedSurfaceR4.PhaseMean.weighted_pullbackField_apply line 106
10. lemma OAI.ClosedSurfaceR4.PhaseMean.weighted_coordinateTarget line 128