DenseModularPair.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.interval_card_le_residue_support line 10
Source documentation
Counting an interval by its quotient and represented residue classes. The second bound separates complete blocks from the final incomplete block.
```
theorem interval_card_le_residue_support (A : Finset ℕ) (N s : ℕ)
    (hs : 0 < s) (hA : A ⊆ Finset.range N) :
    let H := A.image (fun n : ℕ => (n : ZMod s))
…
```
theorem OAI.Problem337.interval_card_le_two_thirds_of_no_modular_pair line 72
Source documentation
If a residue support avoids its reflected copy, then a subset of an interval containing at least a full period has density at most two thirds. The target residue is arbitrary, including self-opposite residues.
```
theorem interval_card_le_two_thirds_of_no_modular_pair
    (A : Finset ℕ) (N s : ℕ) (hs : 0 < s) (hsN : s ≤ N)
    (hA : A ⊆ Finset.range N) (t : ZMod s)
    (hno : ∀ u ∈ A, ∀ v ∈ A, (u : ZMod s) + (v : ZMod s) ≠ t) :
    3 * A.card ≤ 2 * N := by
…
```
Mentions: OAI.Problem337.v
theorem OAI.Problem337.exists_pair_dvd_sum_of_two_thirds line 113
Source documentation
More than two thirds of a positive initial interval contains two elements whose sum is divisible by any prescribed modulus not exceeding the endpoint. The two elements are allowed to agree, as rational-supply lists allow repeats.
```
theorem exists_pair_dvd_sum_of_two_thirds
    (G : Finset ℕ) (N s : ℕ) (hs : 0 < s) (hsN : s ≤ N)
    (hG : G ⊆ Finset.Icc 1 N) (hcard : 2 * N < 3 * G.card) :
    ∃ u ∈ G, ∃ v ∈ G, s ∣ u + v := by
…
```
Mentions: OAI.Problem337.v