OAI/Analysis/HardSphere/Geometry/CandidateConstant.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Lattice.geometricEnvelope_ne_top line 14
2. def OAI.HardSphere.Lattice.candidateConstant line 28
3. def OAI.HardSphere.Lattice.encounterConstant line 30
4. lemma OAI.HardSphere.Lattice.candidateConstant_growth line 32
5. lemma OAI.HardSphere.Lattice.candidateConstant_radius line 35
6. lemma OAI.HardSphere.Lattice.encounterConstant_detour line 37
7. theorem OAI.HardSphere.Lattice.nominal_potential_bound line 40
8. lemma OAI.HardSphere.Lattice.prod_one_add_ofReal_le_exp_sum line 146
9. theorem OAI.HardSphere.Lattice.badComponents_exponential_bound line 162