OAI/Combinatorics/ProgressionColoring/ConstructionArithmetic.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.QuantitativeVanDerWaerden.ConstructionModel.Data line 13
  2. def OAI.QuantitativeVanDerWaerden.ConstructionModel.choose line 17

    Source documentation

    Choose the arithmetic data whose existence is proved by the prime and prime-power scale construction. No coloring or covering data is assumed.

    noncomputable def choose (k : ℕ) (hk : 3 ≤ k) : Data k :=
…

    Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data

  3. def OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda line 21
  4. def OAI.QuantitativeVanDerWaerden.ConstructionModel.groupSize line 23
  5. abbrev OAI.QuantitativeVanDerWaerden.ConstructionModel.Group line 25
  6. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda_pos line 27
  7. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda_ne_zero line 29
  8. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.groupSize_pos line 31
  9. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.groupSize_ne_zero line 34
  10. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.groupSize_neZero line 39

    Source documentation

    Available as a local instance without requiring typeclass inference to reconstruct the prime-scale record from a projected modulus.

    theorem groupSize_neZero {k : ℕ} (s : Data k) : NeZero (groupSize s) :=
…

    Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.groupSize

  11. def OAI.QuantitativeVanDerWaerden.ConstructionModel.groupFintype line 42
  12. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.group_card line 46
  13. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.groupSize_two_le line 49
  14. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.groupSize_eq_prime_pow line 54
  15. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.groupSize_lower line 58
  16. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.prime_step line 62
  17. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.dimension_sq_lt_length line 66

    Source documentation

    The stronger basic-scale inequalities place every prime in the dilation strictly below the prime defining the cyclic group.

    theorem dimension_sq_lt_length {k : ℕ} (h : BasicScales k) :
    (dimension k) ^ 2 < k := by
…
  18. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda_coprime_of_dimension_sq_lt line 75
  19. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda_coprime line 80
  20. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.affine_box_small line 84
  21. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.one_le_log_length line 93