OAI/Probability/MemoryPrecision/CubeBlock.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MemoryPrecision.cube_J_bound line 21
  2. lemma OAI.MemoryPrecision.cube_weighted_ambient line 48
  3. lemma OAI.MemoryPrecision.cubeBall_embedding_subset line 60
  4. lemma OAI.MemoryPrecision.weightedBlock_le_sum line 77
  5. def OAI.MemoryPrecision.CubeBlockConstant line 91
  6. lemma OAI.MemoryPrecision.cubeBlockConstant_one line 92
  7. lemma OAI.MemoryPrecision.cube_constant_scale line 94
  8. def OAI.MemoryPrecision.CubeBlockStatement line 111

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

  9. theorem OAI.MemoryPrecision.cube_block line 119