OAI/Probability/MemoryPrecision/CubeSuccess.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MemoryPrecision.Kernel.source_cube_bound line 21
2. lemma OAI.MemoryPrecision.Kernel.cubePrior_dimension line 44

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

3. def OAI.MemoryPrecision.Kernel.CubeSuccessEstimate line 47
4. def OAI.MemoryPrecision.Kernel.PointwisePrecisionEstimate line 52
5. abbrev OAI.MemoryPrecision.Kernel.SourceCubeStatement line 61
6. theorem OAI.MemoryPrecision.Kernel.source_cube_success line 69