CollisionCounting.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.collisionPairs line 9

Source documentation

Ordered pairs with equal images, including the diagonal.

def collisionPairs {α β : Type*} [DecidableEq α] [DecidableEq β]
    (A : Finset α) (f : α → β) : Finset (α × α) :=
…

def OAI.Problem337.strictCollisionPairs line 14

Source documentation

Ordered collisions between distinct inputs.

def strictCollisionPairs {α β : Type*} [DecidableEq α] [DecidableEq β]
    (A : Finset α) (f : α → β) : Finset (α × α) :=
…

lemma OAI.Problem337.collision_card_eq_sum_square line 18
lemma OAI.Problem337.collision_card_eq_strict_add line 35

theorem OAI.Problem337.card_sq_le_image_card_mul_collisions line 49

Source documentation

Cauchy--Schwarz lower bound for the number of collisions of a finite map.

theorem card_sq_le_image_card_mul_collisions {α β : Type*} [DecidableEq α]
    [DecidableEq β] (A : Finset α) (f : α → β) :
    A.card ^ 2 ≤ (A.image f).card * ((strictCollisionPairs A f).card + A.card) := by
…

Mentions: OAI.Problem337.strictCollisionPairs

theorem OAI.Problem337.strict_collision_lower_bound line 60

Source documentation

If the image has at most half as many elements as the domain, the strict collisions retain at least half the Cauchy--Schwarz lower bound.

theorem strict_collision_lower_bound {α β : Type*} [DecidableEq α]
    [DecidableEq β] (A : Finset α) (f : α → β) {H : ℝ} (hH : 0 < H)
    (himage : ((A.image f).card : ℝ) ≤ H) (hsize : 2 * H ≤ (A.card : ℝ)) :
    (A.card : ℝ) ^ 2 / (2 * H) ≤ ((strictCollisionPairs A f).card : ℝ) := by
…

Mentions: OAI.Problem337.strictCollisionPairs

theorem OAI.Problem337.exceptional_maps_card_le line 77

Source documentation

A generic larger-sieve counting step. A family of maps with small images is small when no distinct pair collides in too many maps. The codomain is allowed to depend on the map (as it does for reduction modulo varying primes).

theorem exceptional_maps_card_le {ι α : Type*} {β : ι → Type*}
    [DecidableEq ι] [DecidableEq α] [∀ i, DecidableEq (β i)]
    (I : Finset ι) (A : Finset α) (f : ∀ i, α → β i)
    {H B : ℝ} (hH : 0 < H) (hB : 0 ≤ B)
    (hsize : 2 * H ≤ (A.card : ℝ))
    (himage : ∀ i ∈ I, ((A.image (f i)).card : ℝ) ≤ H)
    (hpairs : ∀ p ∈ A.offDiag,
      ((I.filter (fun i => f i p.1 = f i p.2)).card : ℝ) ≤ B) :
    (I.card : ℝ) ≤ 2 * H * B := by
…

theorem OAI.Problem337.primeFactors_card_le_log_collision line 124
Source documentation
The number of distinct prime factors of a positive integer is at most its base-two logarithm.
```
theorem primeFactors_card_le_log_collision {d : ℕ} (hd : 0 < d) :
    (d.primeFactors.card : ℝ) ≤ Real.log (d : ℝ) / Real.log 2 := by
…
```

theorem OAI.Problem337.prime_mod_collision_card_le line 140

Source documentation

Distinct positive integers below P collide modulo at most log₂ P primes, even when the tested prime set has no prescribed size.

theorem prime_mod_collision_card_le (I : Finset ℕ) {a b P : ℕ}
    (hprime : ∀ p ∈ I, p.Prime) (ha : 1 ≤ a) (hb : 1 ≤ b)
    (haP : a ≤ P) (hbP : b ≤ P) (hab : a ≠ b) :
    ((I.filter (fun p => a % p = b % p)).card : ℝ) ≤
      Real.log (P : ℝ) / Real.log 2 := by
…

theorem OAI.Problem337.exceptional_primes_card_le line 169

Source documentation

Exceptional-prime bound underlying the rational-divisor supply. If all reductions of A modulo primes in I have size at most H, and |A| ≥ 2H, then |I| ≤ 2H log(P)/log(2) for A ⊆ {1,...,P}.

theorem exceptional_primes_card_le (I A : Finset ℕ) (P : ℕ) {H : ℝ}
    (hprime : ∀ p ∈ I, p.Prime) (hA : ∀ a ∈ A, 1 ≤ a ∧ a ≤ P)
    (hP : 1 ≤ P) (hH : 0 < H) (hsize : 2 * H ≤ (A.card : ℝ))
    (himage : ∀ p ∈ I, ((A.image (fun a => a % p)).card : ℝ) ≤ H) :
    (I.card : ℝ) ≤ 2 * H * (Real.log (P : ℝ) / Real.log 2) := by
…

theorem OAI.Problem337.exceptional_primes_three_quarters line 184

Source documentation

The u^(3/4) exceptional-prime estimate in the supply construction, with all size hypotheses explicit and no analytic prime-distribution input.

theorem exceptional_primes_three_quarters (I A : Finset ℕ) (u P : ℕ)
    (hu : 2 ≤ u) (hprime : ∀ p ∈ I, p.Prime ∧ p ≤ u)
    (hA : ∀ a ∈ A, 1 ≤ a ∧ a ≤ P) (hP : 1 ≤ P)
    (hsize : u ^ 4 ≤ A.card)
    (himage : ∀ p ∈ I,
      ((A.image (fun a => a % p)).card : ℝ) ≤ (p : ℝ) ^ (3 / 4 : ℝ)) :
    (I.card : ℝ) ≤ 2 * (u : ℝ) ^ (3 / 4 : ℝ) *
      (Real.log (P : ℝ) / Real.log 2) := by
…