OAI/Geometry/SurfaceImmersion/Atlas/WeightedRealAlgebra.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Real scalar and vector products used in the quantitative normal formula.

  1. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.mul_real line 12

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

  2. lemma OAI.ClosedSurfaceR4.WeightedEstimates.contDiffOn_dot_real line 29
  3. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.dot_real line 34

    Distinct definitions of this name: OAI/Geometry/Immersion/ClosedSurface/MetricTensors.lean:162 (different declaration text). Qualify references as OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.dot_real@path.

  4. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.smul_real_pi line 48