OAI/Probability/GaussianReplacement/Slab.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentProjection.prod_cubeKernel_scaled line 13
2. lemma OAI.CurrentProjection.normalized_direction line 38
3. lemma OAI.CurrentProjection.gaussian_slab_formula line 42
4. lemma OAI.CurrentProjection.gaussian_slab_limit line 107
5. def OAI.CurrentProjection.fiberPairInverse line 153
6. def OAI.CurrentProjection.fiberSlab line 156
7. def OAI.CurrentProjection.fiberPerpendicularTest line 160
8. lemma OAI.CurrentProjection.measurable_fiberPairInverse line 165
9. lemma OAI.CurrentProjection.measurable_fiberSlab line 169
10. lemma OAI.CurrentProjection.measurable_fiberPerpendicularTest line 177
11. lemma OAI.CurrentProjection.normalized_complement_perpendicular line 185
12. lemma OAI.CurrentProjection.fiberSlab_limit line 192
13. lemma OAI.CurrentProjection.fiberSlab_le line 201
14. lemma OAI.CurrentProjection.fiberSlab_integrated_limit line 217
15. lemma OAI.CurrentProjection.cubeAverage_sphereKernel line 232
16. lemma OAI.CurrentProjection.fiberSlab_tonelli line 239
17. lemma OAI.CurrentProjection.spherical_energy_identity line 268
18. lemma OAI.CurrentProjection.finite_bounded_withDensity line 285
19. lemma OAI.CurrentProjection.weightedSphere_pair_ne line 294
20. lemma OAI.CurrentProjection.spherical_pair_inverse_finite line 301
21. lemma OAI.CurrentProjection.weightedSphere_pair_inverse_finite line 311
22. lemma OAI.CurrentProjection.weightedSphere_projection_ac line 327