WeightedCollision.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Weighted prime collisions

The elementary weighted pair count used in Lemma 2.5 (collision stability). The diagonal is paid for by the largest atom; unequal pairs are paid for by one logarithm of the interval length.

def OAI.Ostmann.primeCollisionWeight line 19
Source documentation
Logarithmic weight of the primes at which two natural numbers collide.
```
noncomputable def primeCollisionWeight (P : Finset ℕ) (a b : ℕ) : ℝ :=
…
```
theorem OAI.Ostmann.primeCollisionWeight_self line 22
theorem OAI.Ostmann.primeCollisionWeight_symm line 26
theorem OAI.Ostmann.primeCollisionWeight_le_log line 34

theorem OAI.Ostmann.weighted_prime_collision_bound_of_budget line 43

Source documentation

The weighted pair count from an off-diagonal logarithmic budget.

theorem weighted_prime_collision_bound_of_budget (P S : Finset ℕ) (μ : ℕ → ℝ) (L m : ℝ)
    (hL : 0 ≤ L) (hP : ∀ p ∈ P, p.Prime) (hμ : ∀ a ∈ S, 0 ≤ μ a)
    (hmass : ∑ a ∈ S, μ a = 1) (hatom : ∀ a ∈ S, μ a ≤ m)
    (hbudget : ∀ a ∈ S, ∀ b ∈ S, a ≠ b → primeCollisionWeight P a b ≤ L) :
    (∑ a ∈ S, ∑ b ∈ S, μ a * μ b * primeCollisionWeight P a b) ≤
      L + m * ∑ p ∈ P, Real.log (p : ℝ) := by
…

Mentions: OAI.Ostmann.primeCollisionWeight

theorem OAI.Ostmann.weighted_prime_collision_bound line 102

Source documentation

Weighted larger-sieve pair bound on the interval [0,X].

theorem weighted_prime_collision_bound (P S : Finset ℕ) (μ : ℕ → ℝ) (X : ℕ) (m : ℝ)
    (hX : 1 ≤ X) (hP : ∀ p ∈ P, p.Prime)
    (hS : ∀ a ∈ S, a ≤ X) (hμ : ∀ a ∈ S, 0 ≤ μ a)
    (hmass : ∑ a ∈ S, μ a = 1) (hatom : ∀ a ∈ S, μ a ≤ m) :
    (∑ a ∈ S, ∑ b ∈ S, μ a * μ b * primeCollisionWeight P a b) ≤
      Real.log (X : ℝ) + m * ∑ p ∈ P, Real.log (p : ℝ) :=
…

Mentions: OAI.Ostmann.primeCollisionWeight

theorem OAI.Ostmann.primeCollisionWeight_le_log_of_dist line 114
Source documentation
The collision budget depends on the diameter, not the position of the interval. This is needed for the translated square-root populations in §3.
```
theorem primeCollisionWeight_le_log_of_dist {P : Finset ℕ} {a b X : ℕ}
    (hab : a ≠ b) (hD : Nat.dist a b ≤ X) (hP : ∀ p ∈ P, p.Prime) :
    primeCollisionWeight P a b ≤ Real.log (X : ℝ) := by
…
```
Mentions: OAI.Ostmann.primeCollisionWeight

theorem OAI.Ostmann.weighted_prime_collision_bound_of_diameter line 125

Source documentation

Weighted larger-sieve pair bound for an arbitrary interval of diameter X.

theorem weighted_prime_collision_bound_of_diameter (P S : Finset ℕ) (μ : ℕ → ℝ)
    (X : ℕ) (m : ℝ) (hX : 1 ≤ X) (hP : ∀ p ∈ P, p.Prime)
    (hD : ∀ a ∈ S, ∀ b ∈ S, Nat.dist a b ≤ X) (hμ : ∀ a ∈ S, 0 ≤ μ a)
    (hmass : ∑ a ∈ S, μ a = 1) (hatom : ∀ a ∈ S, μ a ≤ m) :
    (∑ a ∈ S, ∑ b ∈ S, μ a * μ b * primeCollisionWeight P a b) ≤
      Real.log (X : ℝ) + m * ∑ p ∈ P, Real.log (p : ℝ) :=
…

Mentions: OAI.Ostmann.primeCollisionWeight