ArithmeticCoincidences.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Accidental prime congruences in the arithmetic comparison

These finite estimates implement the two errors in §8: an exact polynomial zero, and an independent sampled prime dividing a nonzero evaluation.

theorem OAI.Ostmann.prime_divisor_card_le line 18

Source documentation

A lower bound on the sizes of the sampled primes converts the logarithmic prime-divisor budget into a bound on their number.

theorem prime_divisor_card_le (P : Finset ℕ) {n : ℕ} (hn : 0 < n)
    (hprime : ∀ p ∈ P, p.Prime) (B K : ℝ) (hB : 0 < B)
    (hsize : ∀ p ∈ P, B ≤ Real.log (p : ℝ))
    (hlog : Real.log (n : ℝ) ≤ K * B) :
    ((P.filter fun p => p ∣ n).card : ℝ) ≤ K := by
…

theorem OAI.Ostmann.prime_divisibility_prior_le line 36

Source documentation

The probability of an independent prime dividing a nonzero integer is bounded by its maximal atom times the number of possible prime divisors.

theorem prime_divisibility_prior_le (P : Finset ℕ) (ν : ℕ → ℝ)
    (β K : ℝ) (hβ : 0 ≤ β) (hν : ∀ p ∈ P, ν p ≤ β)
    (n : ℕ) (hcard : ((P.filter fun p => p ∣ n).card : ℝ) ≤ K) :
    (∑ p ∈ P, if p ∣ n then ν p else 0) ≤ K * β := by
…

theorem OAI.Ostmann.accidental_divisibility_le line 50

Source documentation

Separate the exact-zero event from the independent prime-divisor event. No conditional equidistribution is used in this estimate.

theorem accidental_divisibility_le {X : Type*} [Fintype X]
    (w : X → ℝ) (hw : ∀ x, 0 ≤ w x) (hmass : ∑ x, w x = 1)
    (P : Finset ℕ) (ν : ℕ → ℝ) (hνmass : ∑ p ∈ P, ν p = 1)
    (N : X → ℕ) (β K : ℝ) (hβ : 0 ≤ β) (hK : 0 ≤ K)
    (hν : ∀ p ∈ P, ν p ≤ β)
    (hcard : ∀ x, N x ≠ 0 → ((P.filter fun p => p ∣ N x).card : ℝ) ≤ K) :
    (∑ x, w x * ∑ p ∈ P, if p ∣ N x then ν p else 0) ≤
      (∑ x, w x * if N x = 0 then 1 else 0) + K * β := by
…

theorem OAI.Ostmann.polynomial_prime_coincidence_le line 74

Source documentation

The arithmetic coincidence bound with the exact-zero probability supplied by the proved weighted polynomial root estimate.

theorem polynomial_prime_coincidence_le {A : Type*} [Fintype A] {n : ℕ}
    (value : A → ℚ) (hinj : Function.Injective value)
    (F : MvPolynomial (Fin n) ℚ) (hF : F ≠ 0)
    (μ : Fin n → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a)
    (hmass : ∀ i, ∑ a, μ i a = 1)
    (α : ℝ) (hα : 0 ≤ α) (hmax : ∀ i a, μ i a ≤ α)
    (P : Finset ℕ) (ν : ℕ → ℝ) (hνmass : ∑ p ∈ P, ν p = 1)
    (N : (Fin n → A) → ℕ)
    (hzero : ∀ x, N x = 0 ↔ MvPolynomial.eval (fun i => value (x i)) F = 0)
    (β K : ℝ) (hβ : 0 ≤ β) (hK : 0 ≤ K) (hν : ∀ p ∈ P, ν p ≤ β)
    (hcard : ∀ x, N x ≠ 0 → ((P.filter fun p => p ∣ N x).card : ℝ) ≤ K) :
    (∑ x, productPrior μ x * ∑ p ∈ P, if p ∣ N x then ν p else 0) ≤
…

Mentions: OAI.Ostmann.productPrior