OAI/Probability/MemoryPrecision/PointwiseDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MemoryPrecision.PointwiseDensity line 18

   Also declared: ComparatorChallenges/MemoryPrecision.lean:274 (same declaration text).

2. lemma OAI.MemoryPrecision.measurable_GaussianRegularization line 24
3. lemma OAI.MemoryPrecision.PointwiseDensity_eq_of_tendsto line 32
4. lemma OAI.MemoryPrecision.measurable_PointwiseDensity line 42
5. lemma OAI.MemoryPrecision.GaussianRegularization_nonneg line 65
6. lemma OAI.MemoryPrecision.PointwiseDensity_nonneg line 69