OAI/Combinatorics/SumProduct/Alignment/RoughCube02.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubeDimension.NoLargeCubes line 25
  2. theorem OAI.CubeDimension.no_large_cubes line 40
  3. def OAI.RoughCubeDensity.timeLift line 116
  4. lemma OAI.RoughCubeDensity.timeLift_degree line 119
  5. lemma OAI.RoughCubeDensity.timeLift_vertex line 129
  6. def OAI.RoughCubeDensity.blockOfCube line 145
  7. lemma OAI.RoughCubeDensity.no_dense_indices line 167
  8. theorem OAI.RoughCubeDensity.source_exceptional_decay line 205
  9. theorem OAI.RoughCubeDensity.source_literal_decay line 239
  10. theorem OAI.RoughCubeDensity.rough_step line 270
  11. theorem OAI.RoughCubeDensity.finite_list_uniform line 296