OAI/Combinatorics/Progressions/Lattices/AffineAuxiliaryVariables.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affineCoefficientAllowance line 9
  2. def OAI.Erdos3.normalizedAffineParameter line 11
  3. theorem OAI.Erdos3.affineCoefficientAllowance_pos line 14
  4. theorem OAI.Erdos3.normalizedAffineParameter_identity line 18
  5. theorem OAI.Erdos3.normalizedAffineParameter_abs_le line 23
  6. theorem OAI.Erdos3.affineParameter_abs_upper line 33
  7. theorem OAI.Erdos3.affineParameter_abs_lower line 39
  8. abbrev OAI.Erdos3.AffineAuxiliaryIndex line 53
  9. def OAI.Erdos3.affineAuxiliaryVariables line 55
  10. def OAI.Erdos3.affineAuxiliaryCoefficient line 59
  11. def OAI.Erdos3.affineAuxiliaryExtra line 62
  12. theorem OAI.Erdos3.affineAuxiliaryVariables_coefficient line 66
  13. theorem OAI.Erdos3.affineAuxiliaryVariables_abs_le line 72
  14. theorem OAI.Erdos3.affineAuxiliaryVariables_measurable line 81
  15. theorem OAI.Erdos3.normalizedCubeTuple_affineAuxiliary line 92
  16. theorem OAI.Erdos3.rawCanonicalCubeTuple_affineAuxiliary line 100