OAI/Analysis/HardSphere/Comparison/Affinity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Comparison.integral_mul_le_sqrt line 17
2. lemma OAI.HardSphere.Comparison.memLp_sqrt line 25
3. def OAI.HardSphere.Comparison.affinity line 32
4. lemma OAI.HardSphere.Comparison.affinity_nonneg line 35
5. lemma OAI.HardSphere.Comparison.affinity_integrable line 38
6. lemma OAI.HardSphere.Comparison.sqrt_ratio_product line 43
7. lemma OAI.HardSphere.Comparison.common_density_bound line 59
8. lemma OAI.HardSphere.Comparison.ratio_sqrt_sq line 99
9. lemma OAI.HardSphere.Comparison.memLp_ratio_sqrt line 103
10. theorem OAI.HardSphere.Comparison.common_density_affinity line 112
11. def OAI.HardSphere.Comparison.measureAffinity line 154
12. lemma OAI.HardSphere.Comparison.real_rnDeriv_chain line 158
13. lemma OAI.HardSphere.Comparison.sq_mul_div line 165
14. lemma OAI.HardSphere.Comparison.rnDeriv_density_moment line 170
15. lemma OAI.HardSphere.Comparison.integrable_rnDeriv_density_moment line 183
16. theorem OAI.HardSphere.Comparison.common_measure_affinity line 192