OAI/Geometry/TamingCompatibility/Functional/QuadraticShellLimit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QuadraticShell.lintegral_profile_le_series line 15
2. def OAI.QuadraticShell.dyadicMass line 29
3. lemma OAI.QuadraticShell.dyadicMass_nonneg line 33
4. lemma OAI.QuadraticShell.dyadicMass_bound line 37
5. lemma OAI.QuadraticShell.normalized_profile_le_tsum line 49
6. lemma OAI.QuadraticShell.dyadicMass_tendsto_zero line 71
7. theorem OAI.QuadraticShell.normalized_profile_tendsto_zero line 91
8. lemma OAI.QuadraticShell.profile_le_one line 125
9. lemma OAI.QuadraticShell.measurable_profile line 129
10. lemma OAI.QuadraticShell.integral_profile_toReal line 135
11. lemma OAI.QuadraticShell.integral_profile_normalized_bound line 141
12. lemma OAI.QuadraticShell.integral_profile_normalized_zero line 152