OAI/Probability/ProjectionMoments/RieszPotential.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ProjectionMoments.gaussian_fixed_offset line 13
2. lemma OAI.ProjectionMoments.ambientSphereLaw_nullSingleton line 49
3. lemma OAI.ProjectionMoments.measurable_rieszKernel line 66
4. lemma OAI.ProjectionMoments.rieszKernel_le_inverse_nat line 71
5. lemma OAI.ProjectionMoments.rieszPotential_finite line 87
6. lemma OAI.ProjectionMoments.rieszPotential_ball_control line 116