OAI/Geometry/Immersion/ClosedSurface/MetricTensors.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.RealModes.realMetricTensor_apply line 14
2. lemma OAI.ClosedSurfaceR4.RealModes.realLinearizedTensor_apply line 18
3. def OAI.ClosedSurfaceR4.RealModes.zeroTensor line 22
4. def OAI.ClosedSurfaceR4.RealModes.doubleTensor line 27
5. lemma OAI.ClosedSurfaceR4.RealModes.coordDeriv_realOsc line 31
6. lemma OAI.ClosedSurfaceR4.RealModes.unitMode_half line 39
7. lemma OAI.ClosedSurfaceR4.RealModes.realMetric_realOsc line 51
8. lemma OAI.ClosedSurfaceR4.RealModes.contDiffOn_doubleTensor line 63
9. lemma OAI.ClosedSurfaceR4.RealModes.weighted_gradientAmplitude line 75
10. lemma OAI.ClosedSurfaceR4.RealModes.contDiffOn_dot line 107
11. lemma OAI.ClosedSurfaceR4.RealModes.norm_firstDirection line 112
12. lemma OAI.ClosedSurfaceR4.RealModes.norm_secondDirection line 115
13. lemma OAI.ClosedSurfaceR4.RealModes.weighted_doubleTensor line 118
14. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.mul_real line 145

    Distinct definitions of this name: OAI/Geometry/SurfaceImmersion/Atlas/WeightedRealAlgebra.lean:12 (different declaration text), OAI/Geometry/SurfaceImmersion/Correction/WeightedPolynomialBounds.lean:36 (different declaration text). Qualify references as OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.mul_real@path.

15. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.dot_real line 162

    Distinct definitions of this name: OAI/Geometry/SurfaceImmersion/Atlas/WeightedRealAlgebra.lean:34 (different declaration text). Qualify references as OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.dot_real@path.