OAI/Probability/MemoryPrecision/BallAverages.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MemoryPrecision.gaussianKernel_scale line 18
2. lemma OAI.MemoryPrecision.radialMixture_scale line 33
3. def OAI.MemoryPrecision.BallAverage line 40
4. lemma OAI.MemoryPrecision.ballAverage_measurable line 43
5. lemma OAI.MemoryPrecision.ballAverage_nonneg line 49
6. lemma OAI.MemoryPrecision.ac_ball_eq_closedBall line 54
7. lemma OAI.MemoryPrecision.ae_tendsto_ballAverage line 62
8. lemma OAI.MemoryPrecision.ballAverage_bounded line 77
9. lemma OAI.MemoryPrecision.tendsto_radial_average line 102