OAI/Combinatorics/Progressions/Lattices/ResidueEventOrDescent.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_affine_stability_step line 14
  2. theorem OAI.Erdos3.exists_residue_law_stability_step line 111
  3. def OAI.Erdos3.residuePairStep line 197
  4. def OAI.Erdos3.residuePairValue line 200
  5. def OAI.Erdos3.residuePairMean line 203
  6. theorem OAI.Erdos3.residuePairMean_false line 210
  7. theorem OAI.Erdos3.residuePairMean_true line 222
  8. def OAI.Erdos3.ResiduePairDimensionDrop line 228
  9. theorem OAI.Erdos3.auxiliary_piece_residue_pair line 259
  10. theorem OAI.Erdos3.residuePairStep_const line 327
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.residue_scalar_composed_symbol line 338
  12. theorem OAI.Erdos3.ResiduePairDimensionDrop.scalar_record line 352
  13. theorem OAI.Erdos3.exists_residue_pair_stability_step line 392
  14. theorem OAI.Erdos3.ResiduePairDimensionDrop.of_orbit_eq line 459
  15. theorem OAI.Erdos3.exists_residue_event_or_child_descent line 491