OAI/Geometry/Immersion/ClosedSurface/LocalMean.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ClosedSurfaceR4.PhaseMean.LocalBounds line 19
2. structure OAI.ClosedSurfaceR4.PhaseMean.Budgets line 36
3. def OAI.ClosedSurfaceR4.PhaseMean.inputFactor line 64
4. lemma OAI.ClosedSurfaceR4.PhaseMean.inputFactor_nonneg line 67
5. lemma OAI.ClosedSurfaceR4.PhaseMean.LocalBounds.amplitude_smooth line 73
6. theorem OAI.ClosedSurfaceR4.PhaseMean.LocalBounds.amplitude_bounds line 84
7. def OAI.ClosedSurfaceR4.PhaseMean.outputFactor line 128
8. lemma OAI.ClosedSurfaceR4.PhaseMean.outputFactor_nonneg line 131
9. lemma OAI.ClosedSurfaceR4.PhaseMean.LocalBounds.transport_bound line 137
10. lemma OAI.ClosedSurfaceR4.PhaseMean.LocalBounds.mean_smooth line 152
11. theorem OAI.ClosedSurfaceR4.PhaseMean.LocalBounds.mean_estimates line 163
12. theorem OAI.ClosedSurfaceR4.PhaseMean.actual_local_mean_bounds line 242