OAI/Probability/MemoryPrecision/KernelCube.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MemoryPrecision.Kernel.CubePrior line 23

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

2. instance OAI.MemoryPrecision.Kernel.(instance at line 25) line 25
3. lemma OAI.MemoryPrecision.Kernel.cubeSphere_preserving line 29
4. lemma OAI.MemoryPrecision.Kernel.Policy.eval_comp line 36
5. lemma OAI.MemoryPrecision.Kernel.Policy.pathValue_comp line 46
6. lemma OAI.MemoryPrecision.Kernel.Policy.borel_cube_bound line 51
7. lemma OAI.MemoryPrecision.Kernel.Policy.completed_cube_bound line 81
8. lemma OAI.MemoryPrecision.Kernel.Policy.source_cube_chord_bound line 96