OAI/Probability/GaussianInformation/Kernel/MixedMoments.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.Geometry.tube_ball_bound line 15
2. lemma OAI.KernelPotential.Geometry.inverseMoment_extended_of_tails line 61
3. lemma OAI.KernelPotential.Geometry.angular_integral_ball line 81
4. lemma OAI.KernelPotential.Geometry.inverse_normalized line 136
5. lemma OAI.KernelPotential.Geometry.mixed_integral_shell line 147
6. lemma OAI.KernelPotential.Geometry.ball_bound_zero_null line 191
7. lemma OAI.KernelPotential.Geometry.logarithmic_series_bound line 216
8. lemma OAI.KernelPotential.Geometry.mixed_integral_logarithmic line 248