OAI/Probability/MemoryPrecision/CubeExperiment.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MemoryPrecision.CubeSphere line 20

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

2. lemma OAI.MemoryPrecision.cubeSphere_measurable line 22
3. def OAI.MemoryPrecision.CubeSuccess line 25
4. def OAI.MemoryPrecision.CubeAmbient line 30
5. instance OAI.MemoryPrecision.(instance at line 31) line 31
6. lemma OAI.MemoryPrecision.cubeAmbient_support line 34
7. lemma OAI.MemoryPrecision.cubeAmbient_polynomial line 43
8. lemma OAI.MemoryPrecision.cube_observation_quasi line 54
9. lemma OAI.MemoryPrecision.cube_sample_observation_quasi line 81
10. lemma OAI.MemoryPrecision.cube_estimate_aemeasurable line 89