OAI/Analysis/HardSphere/Kernels/FiniteKernelPi.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HardSphere.Comparison.exists_kernel_pi_fin line 15
2. theorem OAI.HardSphere.Comparison.exists_kernel_pi line 35
3. def OAI.HardSphere.Comparison.finiteKernelPi line 50
4. instance OAI.HardSphere.Comparison.(instance at line 55) line 55
5. lemma OAI.HardSphere.Comparison.finiteKernelPi_apply line 60
6. lemma OAI.HardSphere.Comparison.lintegral_fin_prod line 66
7. lemma OAI.HardSphere.Comparison.lintegral_finite_prod line 93
8. def OAI.HardSphere.Comparison.coordinateKernel line 110
9. instance OAI.HardSphere.Comparison.(instance at line 113) line 113
10. lemma OAI.HardSphere.Comparison.coordinateKernel_apply line 117
11. lemma OAI.HardSphere.Comparison.pi_compProd line 121
12. lemma OAI.HardSphere.Comparison.measurable_kernelPi_integral line 144
13. lemma OAI.HardSphere.Comparison.lintegral_pi_compProd line 150