OAI/Analysis/HardSphere/Geometry/RadiusPotential.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Lattice.radiusActivity_smul line 13
2. lemma OAI.HardSphere.Lattice.ofReal_exp_finset_sum line 20
3. theorem OAI.HardSphere.Lattice.radius_exponential_bound line 26
4. lemma OAI.HardSphere.Lattice.orderedEncounterConstant_one_le line 71
5. lemma OAI.HardSphere.Lattice.radiusEnvelope_le_activity line 80
6. def OAI.HardSphere.Lattice.radiusPotential line 97
7. lemma OAI.HardSphere.Lattice.radiusPotential_nonneg line 99
8. lemma OAI.HardSphere.Lattice.expSlope_one_le line 102
9. lemma OAI.HardSphere.Lattice.small_activity_envelope_le_one line 106
10. lemma OAI.HardSphere.Lattice.radiusPotential_cast line 116
11. theorem OAI.HardSphere.Lattice.small_radius_potential_moment line 120
12. def OAI.HardSphere.Lattice.geometricRadiusWeights line 131
13. lemma OAI.HardSphere.Lattice.geometricRadiusWeights_activity line 134
14. lemma OAI.HardSphere.Lattice.geometricRadiusWeights_envelope line 145
15. lemma OAI.HardSphere.Lattice.succ_le_two_pow line 182
16. lemma OAI.HardSphere.Lattice.radius_polynomial_le line 190
17. lemma OAI.HardSphere.Lattice.geometric_radius_tail_le line 199
18. lemma OAI.HardSphere.Lattice.small_parameters line 228
19. def OAI.HardSphere.Lattice.foldIndex line 260
20. lemma OAI.HardSphere.Lattice.foldIndex_value line 264
21. lemma OAI.HardSphere.Lattice.foldIndex_injective line 271
22. lemma OAI.HardSphere.Lattice.folded_sum_le line 279
23. lemma OAI.HardSphere.Lattice.geometricRadiusWeights_activity_le line 296
24. lemma OAI.HardSphere.Lattice.folded_radius_potential_moment line 303
25. theorem OAI.HardSphere.Lattice.geometric_folded_moment line 317
26. lemma OAI.HardSphere.Lattice.integer_step_lipschitz line 353
27. lemma OAI.HardSphere.Lattice.walk_lipschitz line 373
28. lemma OAI.HardSphere.Lattice.walk_abs_le line 378
29. lemma OAI.HardSphere.Lattice.folded_index_lipschitz line 381