OAI/Geometry/SurfaceImmersion/Correction/CombinedMeanChart.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The concrete fixed data of one chart for the combined mean. This record only groups the geometric, support and polynomial data used by the local construction; its mean estimates are proved from those data.

  1. structure OAI.ClosedSurfaceR4.PhaseMean.CombinedMeanChart line 16
  2. abbrev OAI.ClosedSurfaceR4.PhaseMean.CombinedMeanChart.Operator line 55
  3. def OAI.ClosedSurfaceR4.PhaseMean.CombinedMeanChart.mean line 59
  4. def OAI.ClosedSurfaceR4.PhaseMean.CombinedMeanChart.loss line 63
  5. def OAI.ClosedSurfaceR4.PhaseMean.CombinedMeanChart.exponent line 66
  6. def OAI.ClosedSurfaceR4.PhaseMean.CombinedMeanChart.OperatorBound line 69
  7. theorem OAI.ClosedSurfaceR4.PhaseMean.CombinedMeanChart.majorants line 74