OAI/Geometry/Immersion/ClosedSurface/MeanSupport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClosedSurfaceR4.FiniteMean.MeanBounds.finset_sum line 16
2. lemma OAI.ClosedSurfaceR4.WeightedEstimates.contDiff_of_tsupport_subset line 64
3. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.extend_support line 75
4. lemma OAI.ClosedSurfaceR4.SmallModes.gradientAmplitude_vanishes line 92
5. lemma OAI.ClosedSurfaceR4.SmallModes.modeMeanError_vanishes line 104
6. lemma OAI.ClosedSurfaceR4.PhaseMean.meanTensor_tsupport line 123
7. lemma OAI.ClosedSurfaceR4.PhaseMean.contDiff_meanTensor_of_support line 141
8. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.restrict_open line 155
9. lemma OAI.ClosedSurfaceR4.WeightedEstimates.tsupport_indicator_subset line 162
10. lemma OAI.ClosedSurfaceR4.WeightedEstimates.contDiff_indicator_of_support line 172
11. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.indicator_of_support line 181