OAI/Geometry/TamingCompatibility/Functional/QuadraticShell.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QuadraticShell.profile line 11
2. lemma OAI.QuadraticShell.exists_dyadic_majorant line 13
3. lemma OAI.QuadraticShell.profile_ofReal line 25
4. lemma OAI.QuadraticShell.profile_top line 31
5. lemma OAI.QuadraticShell.profile_majorant line 34
6. lemma OAI.QuadraticShell.dyadic_term_identity line 51
7. theorem OAI.QuadraticShell.lintegral_profile_le line 59