PrimeExceptionalPoints.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Retaining prime atoms on the boundaries of arithmetic root cells

theorem OAI.Ostmann.complexPrimeInterval_exceptional_bound line 12

Source documentation

Changing the weight at finitely many primes costs their actual atom masses. The estimate is uniform in the residue class and keeps endpoints.

theorem complexPrimeInterval_exceptional_bound (q a : ℕ) (u v : ℝ)
    (w g : ℝ → ℂ) (S : Finset ℕ) (B : ℝ) (hB : 0 ≤ B)
    (hbound : ∀ p ∈ Finset.Ioc ⌊Real.exp u⌋₊ ⌊Real.exp v⌋₊,
      p.Prime → Nat.ModEq q p a → ‖w (Real.log p) - g (Real.log p)‖ ≤ B)
    (heq : ∀ p ∈ Finset.Ioc ⌊Real.exp u⌋₊ ⌊Real.exp v⌋₊,
      p.Prime → Nat.ModEq q p a → p ∉ S → w (Real.log p) = g (Real.log p)) :
    ‖complexPrimeInterval q a u v w - complexPrimeInterval q a u v g‖ ≤
      (S.card : ℝ) * B * Real.exp (-u) := by
…

Mentions: OAI.Ostmann.complexPrimeInterval

theorem OAI.Ostmann.prime_boundary_card_le line 70
Source documentation
The exceptional primes lying on real root boundaries inject into the boundary set, so their count never exceeds the number of cuts.
```
theorem prime_boundary_card_le (T : Finset ℕ) (S : Finset ℝ) :
    (T.filter (fun p : ℕ => (p : ℝ) ∈ S)).card ≤ S.card := by
…
```