OAI/Analysis/HardSphere/Geometry/PathEncounter.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Lattice.accepted_charge_environment_bound line 15
2. def OAI.HardSphere.Lattice.pathEncounter line 69
3. def OAI.HardSphere.Lattice.pathKernelMoment line 73
4. lemma OAI.HardSphere.Lattice.goodPathKernel_moment_noises line 77
5. lemma OAI.HardSphere.Lattice.detourSample_charge line 89
6. theorem OAI.HardSphere.Lattice.good_kernel_average_le_folded line 116
7. theorem OAI.HardSphere.Lattice.good_kernel_uniform_constants line 179