OAI/Geometry/Immersion/ClosedSurface/MeanBilinearity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.QuadraticMean.zeroPair_add_left line 12
2. lemma OAI.ClosedSurfaceR4.QuadraticMean.zeroPair_add_right line 16
3. lemma OAI.ClosedSurfaceR4.QuadraticMean.zeroPair_smul_left line 22
4. lemma OAI.ClosedSurfaceR4.QuadraticMean.zeroPair_smul_right line 26
5. lemma OAI.ClosedSurfaceR4.QuadraticMean.zeroPair_comm line 32
6. lemma OAI.ClosedSurfaceR4.RealModes.gradientAmplitude_base_decomposition line 48
7. lemma OAI.ClosedSurfaceR4.RealModes.evaluate_phaseZeroTensor line 62
8. lemma OAI.ClosedSurfaceR4.RealModes.derivativeAmplitude_coordinate line 73
9. lemma OAI.ClosedSurfaceR4.RealModes.phaseZeroTensor_coordinate line 84
10. lemma OAI.ClosedSurfaceR4.RealModes.freePhase_zeroTensor line 99