OAI/Probability/MemoryPrecision/FiberDensity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MemoryPrecision.PiGaussianConvolution line 20
2. lemma OAI.MemoryPrecision.piGaussianConvolution_eq line 23
3. lemma OAI.MemoryPrecision.ae_tendsto_piGaussianConvolution line 32
4. lemma OAI.MemoryPrecision.GaussianRegularization_eq_convolution line 56
5. lemma OAI.MemoryPrecision.ae_tendsto_GaussianRegularization line 67
6. lemma OAI.MemoryPrecision.reciprocal_nat_tendsto line 76
7. lemma OAI.MemoryPrecision.pointwiseDensity_fiber line 83
8. lemma OAI.MemoryPrecision.pointwiseDensity_fullRank line 99