OAI/Probability/PosteriorReplicas/Gaussian/RadialIntegrals.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.lintegral_pos_smul line 10
2. lemma OAI.PosteriorReplicas.lintegral_Ioi_pos_mul line 23
3. lemma OAI.PosteriorReplicas.radial_lintegral_scale line 39
4. lemma OAI.PosteriorReplicas.gaussianPolarRadius_mass_integral line 59
5. lemma OAI.PosteriorReplicas.lintegral_gaussianPolarRadius line 73
6. lemma OAI.PosteriorReplicas.gaussianRadialDensity_mul line 86
7. lemma OAI.PosteriorReplicas.radial_power_gaussian_product line 96
8. lemma OAI.PosteriorReplicas.radial_gaussian_integral line 108
9. lemma OAI.PosteriorReplicas.sphere_area line 129