OAI/Geometry/Immersion/ClosedSurface/QuadraticSupport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ClosedSurfaceR4.RealModes.QuadraticLabel line 15
2. def OAI.ClosedSurfaceR4.RealModes.quadraticPhase line 17
3. def OAI.ClosedSurfaceR4.RealModes.quadraticAmplitude line 21
4. def OAI.ClosedSurfaceR4.RealModes.quadraticSupport line 27
5. lemma OAI.ClosedSurfaceR4.RealModes.nonzeroPhaseSum_eq_quadraticFamily line 31
6. lemma OAI.ClosedSurfaceR4.RealModes.derivativeAmplitude_zero_of_notMem line 55
7. lemma OAI.ClosedSurfaceR4.RealModes.phasePlusTensor_tsupport line 60
8. lemma OAI.ClosedSurfaceR4.RealModes.phaseMinusTensor_tsupport line 70
9. lemma OAI.ClosedSurfaceR4.RealModes.quadraticAmplitude_tsupport line 81
10. lemma OAI.ClosedSurfaceR4.RealModes.quadraticAmplitude_smooth line 95