OAI/Geometry/Immersion/ClosedSurface/ComplexPullback.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ClosedSurfaceR4.PhaseMean.ComplexTensor line 14
2. def OAI.ClosedSurfaceR4.PhaseMean.complexEvaluate line 16
3. def OAI.ClosedSurfaceR4.PhaseMean.complexPullback line 23
4. def OAI.ClosedSurfaceR4.PhaseMean.complexPullbackField line 30
5. lemma OAI.ClosedSurfaceR4.PhaseMean.complexPullback_apply line 33
6. lemma OAI.ClosedSurfaceR4.PhaseMean.complexEvaluate_pullback line 36
7. lemma OAI.ClosedSurfaceR4.PhaseMean.complexPullback_comp line 51
8. lemma OAI.ClosedSurfaceR4.PhaseMean.complexPullback_id line 57
9. lemma OAI.ClosedSurfaceR4.PhaseMean.realPart_complexPullback line 63
10. lemma OAI.ClosedSurfaceR4.PhaseMean.realMode_complexPullback line 69
11. lemma OAI.ClosedSurfaceR4.PhaseMean.complexPullbackField_inverse line 74
12. lemma OAI.ClosedSurfaceR4.PhaseMean.oscillating_pullback_inverse line 84
13. lemma OAI.ClosedSurfaceR4.PhaseMean.contDiffOn_complexEvaluate line 97
14. lemma OAI.ClosedSurfaceR4.PhaseMean.contDiffOn_complexPullbackField_apply line 110
15. def OAI.ClosedSurfaceR4.PhaseMean.coordinateTarget line 121
16. lemma OAI.ClosedSurfaceR4.PhaseMean.contDiffOn_coordinateTarget line 124