OAI/NumberTheory/EgyptianFractions/RoughModulusCollision.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.large_collision_maps_card_le line 12

   Source documentation

   A collision-energy threshold, rather than a small-image hypothesis, also permits the larger-sieve double count. The diagonal is removed before using the bound on how many maps can identify two distinct inputs.

   theorem large_collision_maps_card_le {ι α : Type*} {β : ι → Type*}
       [DecidableEq ι] [DecidableEq α] [∀ i, DecidableEq (β i)]
       (I : Finset ι) (A : Finset α) (f : ∀ i, α → β i)
       {H R : ℝ} (hH : 0 < H) (hR : 0 ≤ R)
       (hsize : 2 * H ≤ (A.card : ℝ))
       (henergy : ∀ i ∈ I,
         (A.card : ℝ) ^ 2 ≤ H * ((collisionPairs A (f i)).card : ℝ))
       (hpairs : ∀ p ∈ A.offDiag,
         ((I.filter (fun i => f i p.1 = f i p.2)).card : ℝ) ≤ R) :
       (I.card : ℝ) ≤ 2 * H * R := by
   …

   Mentions: OAI.Problem337.collisionPairs

2. theorem OAI.Problem337.moduli_energy_card_le_of_divisor_count line 70

   Source documentation

   For arbitrary moduli, each off-diagonal collision gives a divisor of a positive difference. The predicate Q can restrict the divisors to rough integers; the difference itself need not be rough.

   theorem moduli_energy_card_le_of_divisor_count
       (I A : Finset ℕ) (P : ℕ) (X : ℝ) (Q : ℕ → Prop) [DecidablePred Q]
       {H R : ℝ} (hH : 0 < H) (hR : 0 ≤ R)
       (hA : ∀ a ∈ A, 1 ≤ a ∧ a ≤ P)
       (hI : ∀ q ∈ I, (q : ℝ) ≤ X ∧ Q q)
       (hsize : 2 * H ≤ (A.card : ℝ))
       (henergy : ∀ q ∈ I,
         (A.card : ℝ) ^ 2 ≤ H * ((collisionPairs A (fun a => a % q)).card : ℝ))
       (hdivisors : ∀ n : ℕ, 0 < n → n ≤ P →
         ((n.divisors.filter (fun d : ℕ => (d : ℝ) ≤ X ∧ Q d)).card : ℝ) ≤ R) :
       (I.card : ℝ) ≤ 2 * H * R := by
   …

   Mentions: OAI.Problem337.collisionPairs

3. theorem OAI.Problem337.moduli_rpow_energy_card_le line 107

   Source documentation

   A common divisor list on a modulus block turns a power-size collision exception into a sparse set of moduli. This is applicable to every modulus, not only primes, and retains the genuine restricted-divisor-count input.

   theorem moduli_rpow_energy_card_le
       (I A : Finset ℕ) (P : ℕ) (X θ : ℝ) (Q : ℕ → Prop) [DecidablePred Q]
       {R : ℝ} (hX : 0 < X) (hθ : 0 ≤ θ) (hR : 0 ≤ R)
       (hA : ∀ a ∈ A, 1 ≤ a ∧ a ≤ P)
       (hI : ∀ q ∈ I, (q : ℝ) ≤ X ∧ Q q)
       (hsize : 2 * X ^ θ ≤ (A.card : ℝ))
       (henergy : ∀ q ∈ I, (A.card : ℝ) ^ 2 ≤
         (q : ℝ) ^ θ * ((collisionPairs A (fun a => a % q)).card : ℝ))
       (hdivisors : ∀ n : ℕ, 0 < n → n ≤ P →
         ((n.divisors.filter (fun d : ℕ => (d : ℝ) ≤ X ∧ Q d)).card : ℝ) ≤ R) :
       (I.card : ℝ) ≤ 2 * X ^ θ * R := by
   …

   Mentions: OAI.Problem337.collisionPairs