OAI/Analysis/HardSphere/Cutoffs/CloseLabels.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.TightCutoff.closeLabels line 20
2. lemma OAI.HardSphere.TightCutoff.mem_closeLabels_of_near line 25
3. def OAI.HardSphere.TightCutoff.orbitalCutoff line 31
4. lemma OAI.HardSphere.TightCutoff.orbitalCutoff_real line 34
5. lemma OAI.HardSphere.TightCutoff.orbitalCutoff_clearance line 43
6. lemma OAI.HardSphere.TightCutoff.weighted_near_le line 47
7. lemma OAI.HardSphere.TightCutoff.rawCutoff_mass_pointwise line 66
8. lemma OAI.HardSphere.TightCutoff.localized_mass_pointwise line 86
9. lemma OAI.HardSphere.TightCutoff.near_sum_integral_le line 99
10. lemma OAI.HardSphere.TightCutoff.localized_mass_lower line 112
11. lemma OAI.HardSphere.TightCutoff.norm_add_sq_le_two line 140
12. lemma OAI.HardSphere.TightCutoff.orbitalCutoff_derivative_le line 145
13. lemma OAI.HardSphere.TightCutoff.localized_gradient_pointwise line 167
14. lemma OAI.HardSphere.TightCutoff.derivative_fiber_integrable line 191
15. lemma OAI.HardSphere.TightCutoff.orbital_derivative_integrable line 199
16. lemma OAI.HardSphere.TightCutoff.localized_gradient_integral_le line 204