OAI/Combinatorics/ProgressionColoring/KeyMultiplicity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuantitativeVanDerWaerden.affine_norm_band_card_le_two line 17

   Source documentation

   Squared-separated points on an affine line in one half-open norm band.

   theorem affine_norm_band_card_le_two {ι : Type uIndex} {D : ℕ} (s : Finset ι)
       (t : ι → ℝ) (A B : Vec D) (m : ℝ)
       (hsep : (s : Set ι).Pairwise fun i j =>
         1 ≤ distSq (fun d => A d + t i * B d) (fun d => A d + t j * B d))
       (hband : ∀ i ∈ s,
         m ≤ normSq (fun d => A d + t i * B d) ∧
         normSq (fun d => A d + t i * B d) < m + 1) :
       s.card ≤ 2 := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.Vec, OAI.QuantitativeVanDerWaerden.distSq, OAI.QuantitativeVanDerWaerden.normSq

2. theorem OAI.QuantitativeVanDerWaerden.affine_norm_band_card_le_four line 44
3. def OAI.QuantitativeVanDerWaerden.geometricKey line 55

   Source documentation

   The literal box label and integer squared-norm band.

   def geometricKey {X : Type uX} {Box : Type uBox} {D : ℕ}
       (box : X → Box) (point : X → Vec D) (x : X) : Box × ℤ :=
   …

   Mentions: OAI.QuantitativeVanDerWaerden.Vec

4. theorem OAI.QuantitativeVanDerWaerden.geometricKey_band line 59
5. theorem OAI.QuantitativeVanDerWaerden.same_geometricKey_card_le_four line 69

   Source documentation

   No consecutive-index assumption is made on the selected key occurrences.

   theorem same_geometricKey_card_le_four {ι : Type uIndex} {Box : Type uBox} {D : ℕ}
       (s : Finset ι) (t : ι → ℝ) (box : ι → Box) (point : ι → Vec D)
       (key : Box × ℤ) (hkey : ∀ i ∈ s, geometricKey box point i = key)
       (hsep : (s : Set ι).Pairwise fun i j => 1 ≤ distSq (point i) (point j))
       (A B : Vec D) (haffine : ∀ i ∈ s, point i = fun d => A d + t i * B d) :
       s.card ≤ 4 := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.Vec, OAI.QuantitativeVanDerWaerden.geometricKey, OAI.QuantitativeVanDerWaerden.distSq

6. def OAI.QuantitativeVanDerWaerden.scaledYRep line 84

   Source documentation

   The actual scale used by the second representative system.

   def scaledYRep (q D dilation : ℕ) (n : CyclicGroup q D) : Vec D :=
   …

   Mentions: OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.Vec

7. def OAI.QuantitativeVanDerWaerden.yGeometricKey line 87
8. theorem OAI.QuantitativeVanDerWaerden.yGeometricKey_fiber_card_le_four line 91
9. def OAI.QuantitativeVanDerWaerden.secondBox line 149

   Source documentation

   The actual coordinatewise second-system box label.

   def secondBox (mesh : AdaptiveMesh) (q D dilation : ℕ)
       (n : CyclicGroup q D) : Fin D → mesh.Label :=
   …

   Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup

10. def OAI.QuantitativeVanDerWaerden.perturbationKey line 153
11. theorem OAI.QuantitativeVanDerWaerden.secondBox_same_distance line 157
12. theorem OAI.QuantitativeVanDerWaerden.perturbationKey_fiber_card_le_four line 172

    Source documentation

    Every literal geometric key occurs at most four times on an actual nonconstant cyclic progression. The prime-power hypothesis supplies distinct terms, the mesh supplies the width bound, and coprime dilation supplies squared separation; no affinity or key-multiplicity conclusion is assumed.

    theorem perturbationKey_fiber_card_le_four (mesh : AdaptiveMesh)
        {P e D dilation k : ℕ} (hP : P.Prime) (hk : k ≤ P)
        (hunit : Nat.Coprime dilation ((P ^ e) ^ D))
        (hsmall : 2 * (k : ℝ) * mesh.H < 1)
        (a d : CyclicGroup (P ^ e) D) (hd : d ≠ 0)
        (key : (Fin D → mesh.Label) × ℤ) :
        ((Finset.range k).filter fun j : ℕ =>
          perturbationKey mesh (P ^ e) D dilation
            (a + (j : CyclicGroup (P ^ e) D) * d) = key).card ≤ 4 := by
    …

    Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.perturbationKey

13. theorem OAI.QuantitativeVanDerWaerden.perturbationKey_fin_fiber_card_le_four line 190

    Source documentation

    The same literal-key bound on the finite index type used by the Bernoulli perturbation. This is only the bijection between Fin k and range k; the geometric argument is reused unchanged.

    theorem perturbationKey_fin_fiber_card_le_four (mesh : AdaptiveMesh)
        {P e D dilation k : ℕ} (hP : P.Prime) (hk : k ≤ P)
        (hunit : Nat.Coprime dilation ((P ^ e) ^ D))
        (hsmall : 2 * (k : ℝ) * mesh.H < 1)
        (a d : CyclicGroup (P ^ e) D) (hd : d ≠ 0)
        (key : (Fin D → mesh.Label) × ℤ) :
        (Finset.univ.filter fun j : Fin k =>
          perturbationKey mesh (P ^ e) D dilation
            (a + (j.val : CyclicGroup (P ^ e) D) * d) = key).card ≤ 4 := by
    …

    Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.perturbationKey