OAI/Geometry/Immersion/ClosedSurface/ModeScaling.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.SmallModes.partial_const_smul line 12
2. lemma OAI.ClosedSurfaceR4.SmallModes.reducedKx_smul line 18
3. lemma OAI.ClosedSurfaceR4.SmallModes.reducedKy_smul line 25
4. lemma OAI.ClosedSurfaceR4.SmallModes.component_const_smul line 32
5. lemma OAI.ClosedSurfaceR4.SmallModes.amplitudeCorrection_smul line 35
6. lemma OAI.ClosedSurfaceR4.SmallModes.initialAmplitude_smul line 50
7. lemma OAI.ClosedSurfaceR4.SmallModes.conjugatedMetric_smul line 63
8. lemma OAI.ClosedSurfaceR4.SmallModes.conjugatedD_smul line 70
9. theorem OAI.ClosedSurfaceR4.SmallModes.modeApprox_smul line 78
10. lemma OAI.ClosedSurfaceR4.RealModes.freeSeed_scale line 121
11. lemma OAI.ClosedSurfaceR4.RealModes.chartFreeAmplitude_scale line 128
12. lemma OAI.ClosedSurfaceR4.RealModes.phaseFreeFamily_scale line 145
13. lemma OAI.ClosedSurfaceR4.RealModes.derivativeAmplitude_real_smul line 162
14. lemma OAI.ClosedSurfaceR4.RealModes.phaseZeroTensor_real_smul line 172
15. lemma OAI.ClosedSurfaceR4.RealModes.phaseFreeZero_scale line 181