OAI/Combinatorics/Progressions/Lattices/AnchoredCubeResidueWidths.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.BooleanCubeKernel.cubeModePolynomialBudget_pos line 15
  2. theorem OAI.Erdos3.BooleanCubeKernel.affineSite_intCast line 20
  3. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_bounded_integer_mode line 26
  4. theorem OAI.Erdos3.BooleanCubeKernel.exists_selected_affine_mode_rows line 60
  5. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_cube_local_removal line 109
  6. theorem OAI.Erdos3.BooleanCubeKernel.affine_cube_mode_residue_removal line 179
  7. theorem OAI.Erdos3.BooleanCubeKernel.anchored_affine_cube_mode_residue_removal line 249
  8. theorem OAI.Erdos3.BooleanCubeKernel.affine_cube_mode_smooth_removal line 322
  9. theorem OAI.Erdos3.BooleanCubeKernel.affine_cube_residue_removal_of_widths line 395
  10. theorem OAI.Erdos3.BooleanCubeKernel.anchored_affine_cube_residue_removal_of_widths line 489