OAI/Probability/MemoryPrecision/FiniteDensity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MemoryPrecision.MatrixLabelReference line 20

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

2. def OAI.MemoryPrecision.ProjectionLaw line 42

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

3. def OAI.MemoryPrecision.ProjectedEllipsoid line 77

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

4. def OAI.MemoryPrecision.ProjectionNormScale line 90

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

5. lemma OAI.MemoryPrecision.isClosed_projectedEllipsoid line 97
6. lemma OAI.MemoryPrecision.projectionLaw_ellipsoid_compl line 115
7. lemma OAI.MemoryPrecision.projectionNormScale_pos line 133
8. lemma OAI.MemoryPrecision.moment_root_eq_scale line 146
9. lemma OAI.MemoryPrecision.exact_finite_density line 189
10. def OAI.MemoryPrecision.FiniteDensityStatement line 247

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

11. theorem OAI.MemoryPrecision.finite_density line 272