OAI/Geometry/Perimeter/Regularity/TendstoLintegralNormOfL2.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RPIKernel.tendsto_lintegral_norm_of_L2 line 16
2. theorem OAI.RPIKernel.sobolev_limit line 49
3. theorem OAI.RPISingularHarnack.wholeBoundary_nonlinear_approximation line 88
4. theorem OAI.RPISingularHarnack.wholeBoundary_sublevel_sobolev line 199
5. lemma OAI.RPIKernel.weighted_sublevel_gradient_bound line 249
6. lemma OAI.RPIKernel.integral_norm_sublevel_bound line 282
7. theorem OAI.RPISingularHarnack.wholeBoundary_sublevel_L1 line 322
8. theorem OAI.RPISingularHarnack.exists_interior_cutoff_constant line 439
9. lemma OAI.RPIIteration.sublevel_step_division line 503
10. lemma OAI.RPIIteration.sublevel_step_factor line 509