OAI/Geometry/PeriodicTiling/ResidueCountBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PeriodicTilingThree.one_sub_pow_mul_linear_le_one line 10
  2. theorem OAI.PeriodicTilingThree.scalar_half_bound line 31
  3. theorem OAI.PeriodicTilingThree.residue_block_bound line 37
  4. theorem OAI.PeriodicTilingThree.residue_failure_block_bound line 43
  5. theorem OAI.PeriodicTilingThree.union_bound_from_block line 50
  6. theorem OAI.PeriodicTilingThree.residue_union_bound_32000 line 62
  7. theorem OAI.PeriodicTilingThree.residue_union_bound_of_large_exponent line 67
  8. theorem OAI.PeriodicTilingThree.residue_cube_64 line 73
  9. theorem OAI.PeriodicTilingThree.residue_matching_budget_64 line 75