OAI/Combinatorics/Progressions/Estimates/NativeDetectorContradictionSpec.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_controlled_prescribed_square_model line 16
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_controlled_prescribed_square_family line 135
  3. theorem OAI.Erdos3.PositiveShiftBasis.exists_native_partner_intervals line 220
  4. structure OAI.Erdos3.RationalFilteredNilmanifold.SquareModelData line 282
  5. def OAI.Erdos3.RationalFilteredNilmanifold.SquareModelData.fullModel line 297
  6. def OAI.Erdos3.RationalFilteredNilmanifold.SquareModelData.quotientModel line 303
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.SquareModelData.quotientModel_adapted line 309
  8. theorem OAI.Erdos3.PositiveShiftBasis.exists_prescribed_lower_inputs line 336
  9. def OAI.Erdos3.PositiveShiftBasis.PrescribedCommonFactorizationSpec line 490
  10. def OAI.Erdos3.PositiveShiftBasis.FactoredPositiveShiftContradictionSpec line 571
  11. def OAI.Erdos3.PositiveShiftBasis.NativePartnerContradictionSpec line 648
  12. def OAI.Erdos3.PositiveShiftBasis.NativePartnerPairContradictionSpec line 700
  13. def OAI.Erdos3.PositiveShiftBasis.TwoSiteModelContradictionSpec line 750
  14. def OAI.Erdos3.PositiveShiftBasis.NativeDetectorContradictionSpec line 802