OAI/Analysis/HardSphere/Geometry/SliceNormSq.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.killed_endpoint_quadratic line 17
2. lemma OAI.HardSphere.killed_endpoint_quadratic_function line 29
3. def OAI.HardSphere.sliceNormSq line 60
4. lemma OAI.HardSphere.sliceNormSq_nonneg line 63
5. lemma OAI.HardSphere.sliceNormSq_measurable line 66
6. lemma OAI.HardSphere.memLp_slice_ae line 73
7. lemma OAI.HardSphere.bath_slice_quadratic_ae line 83