OAI/Geometry/Immersion/ClosedSurface/CrossModes.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.RealModes.phaseZeroTensor line 17
2. def OAI.ClosedSurfaceR4.RealModes.phaseDoubleTensor line 23
3. def OAI.ClosedSurfaceR4.RealModes.phasePlusTensor line 28
4. def OAI.ClosedSurfaceR4.RealModes.phaseMinusTensor line 33
5. lemma OAI.ClosedSurfaceR4.RealModes.displacement_doubleTensor line 38
6. lemma OAI.ClosedSurfaceR4.RealModes.displacement_crossTensor line 46
7. def OAI.ClosedSurfaceR4.RealModes.zeroPhaseSum line 56
8. def OAI.ClosedSurfaceR4.RealModes.nonzeroPhaseSum line 60
9. lemma OAI.ClosedSurfaceR4.RealModes.realMetric_sumDisplacement line 69
10. lemma OAI.ClosedSurfaceR4.RealModes.realLinearized_sum_right line 82
11. theorem OAI.ClosedSurfaceR4.RealModes.finite_phase_metric_identity line 93
12. lemma OAI.ClosedSurfaceR4.QuadraticMean.contDiffOn_derivativeAmplitude line 121
13. lemma OAI.ClosedSurfaceR4.QuadraticMean.weighted_real_complex line 132
14. lemma OAI.ClosedSurfaceR4.QuadraticMean.weighted_derivativeAmplitude line 147
15. lemma OAI.ClosedSurfaceR4.QuadraticMean.weighted_halfDot line 176
16. lemma OAI.ClosedSurfaceR4.RealModes.contDiffOn_phasePlusTensor line 194
17. lemma OAI.ClosedSurfaceR4.RealModes.contDiffOn_phaseMinusTensor line 203
18. theorem OAI.ClosedSurfaceR4.RealModes.weighted_phaseCrossTensor line 215