OAI/Combinatorics/SumProduct/Alignment/RoughCube01.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubeConstant.constant_thinning line 20
  2. def OAI.RoughCubeBlock.time line 83
  3. lemma OAI.RoughCubeBlock.time_subspace line 86
  4. structure OAI.RoughCubeBlock.Block line 98
  5. def OAI.RoughCubeBlock.Block.subspace line 130
  6. def OAI.RoughCubeBlock.initial line 157
  7. def OAI.RoughCubeBlock.Block.restrict line 167
  8. lemma OAI.CubeCharacter.degree_character line 198
  9. def OAI.CubeCharacter.coefficients line 210
  10. theorem OAI.CubeCharacter.character_tools line 217