OAI/Combinatorics/Progressions/Lattices/RetainedAffineCommonCover.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.modeResidueSideThreshold line 12
  2. theorem OAI.Erdos3.modeResidueSideThreshold_bounds line 15
  3. theorem OAI.Erdos3.modeResidueWidth_mesh line 30
  4. theorem OAI.Erdos3.selectedResidueSmoothWeight_pos_of_threshold line 58
  5. theorem OAI.Erdos3.exists_mode_residue_threshold_exp_budget line 91
  6. theorem OAI.Erdos3.BooleanCubeKernel.exists_cube_residue_threshold_exp_budget line 131
  7. theorem OAI.Erdos3.BooleanCubeKernel.affine_cube_residue_removal_at_error line 172
  8. theorem OAI.Erdos3.BooleanCubeKernel.anchored_affine_cube_residue_removal_at_error line 253
  9. theorem OAI.Erdos3.VectorPolynomial.affine_coefficient_amplitude_residue_removal_at_error line 334
  10. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_cube_residue_uniform_removal line 414
  11. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_cube_ambient_residue_removal line 475
  12. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_cube_congruence_removal line 537
  13. def OAI.Erdos3.BooleanCubeKernel.affineCubeModeFactors line 596
  14. theorem OAI.Erdos3.BooleanCubeKernel.not_affineCubeModeFactors_iff line 606
  15. theorem OAI.Erdos3.BooleanCubeKernel.affineCubeModeFactors_bounded line 629
  16. theorem OAI.Erdos3.BooleanCubeKernel.exists_retained_affine_layer_cover line 659
  17. theorem OAI.Erdos3.BooleanCubeKernel.exists_retained_affine_common_cover line 704