OAI/Analysis/HardSphere/Comparison/SumMoment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Comparison.retainedFiniteSum line 14
2. instance OAI.HardSphere.Comparison.retainedFiniteSum_finite line 16
3. lemma OAI.HardSphere.Comparison.retainedFiniteSum_snd line 20
4. lemma OAI.HardSphere.Comparison.retainedFiniteSum_density line 25
5. theorem OAI.HardSphere.Comparison.finite_sum_second_moment line 42