OAI/Analysis/HardSphere/Kernels/KernelDensity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Comparison.successKernel_restrict_le line 15
2. lemma OAI.HardSphere.Comparison.successful_marginal_le line 23
3. lemma OAI.HardSphere.Comparison.normalizer_positive_of_uniform_success line 44
4. lemma OAI.HardSphere.Comparison.restricted_le_normalized line 59
5. lemma OAI.HardSphere.Comparison.successful_marginal_le_reference line 67