OAI/Geometry/SurfaceImmersion/Correction/UniformNormalizedMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit constants for the normalized geometric metric mean, independent of its oscillation and amplitude scales.

  1. def OAI.ClosedSurfaceR4.RealModes.normalizedMeanBudget line 17
  2. lemma OAI.ClosedSurfaceR4.RealModes.normalizedMeanBudget_nonneg line 21
  3. theorem OAI.ClosedSurfaceR4.RealModes.normalizedMeanBudget_bound line 26
  4. theorem OAI.ClosedSurfaceR4.RealModes.normalizedMeanBudget_difference line 70