OAI/Geometry/SurfaceImmersion/Correction/FiniteMeanSums.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Assemble finitely many actual mean operators with a common derivative loss while retaining their scale-independent majorants.

  1. lemma OAI.ClosedSurfaceR4.FiniteMean.MeanBounds.mono_loss line 15
  2. lemma OAI.ClosedSurfaceR4.FiniteMean.rescaledMean_finset line 28
  3. lemma OAI.ClosedSurfaceR4.FiniteMean.MeanBounds.finset_rescaled line 35