PagePopulationDecay.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Decay of the exceptional Page-kernel population

At the manuscript's threshold R = (log X)^100, the already proved population bound is smaller than X / (log X)^40, uniformly in the small common-center denominator. No analytic estimate is added here.

theorem OAI.Ostmann.exists_page_population_error_cutoff line 20

Source documentation

One cutoff absorbs both square-root population errors uniformly for all denominators bounded by exp(η L), with η ≤ 1/1000.

theorem exists_page_population_error_cutoff :
    ∃ L₀ : ℝ, 1 ≤ L₀ ∧ ∀ L η : ℝ, L₀ ≤ L → η ≤ 1 / 1000 →
      ∀ m : ℕ, (m : ℝ) ≤ Real.exp (η * L) →
        Real.exp L / Real.sqrt (L ^ (100 : ℕ)) +
            2 * Real.sqrt (Real.exp L * m) + m ≤
          4 * (Real.exp L / L ^ (40 : ℕ)) := by
…

theorem OAI.Ostmann.exists_page_population_decay line 78

Source documentation

The actual exceptional pair family at R = L^100 has negligible population on the endpoint-product scale exp L / L^6. The exponent forty retains a fixed reserve for the subsequent common-center selections.

theorem exists_page_population_decay :
    ∃ C L₀ : ℝ, 0 < C ∧ 1 ≤ L₀ ∧
      ∀ (P : PublishedProgressionInput) (Q₀ : ℕ) (L η : ℝ),
      L₀ ≤ L → η ≤ 1 / 1000 →
      ∀ (S T : Finset ℤ) (f g : ℤ → ℤ) (r s : ℤ → ℕ) (m : ℕ) (h : ℤ),
      0 < m → (m : ℝ) ≤ Real.exp (η * L) →
      (∀ x ∈ S, f x ≠ 0) → (∀ y ∈ T, g y ≠ 0) →
      h.natAbs.Coprime m →
      (∀ x ∈ S, f x * (r x : ℤ) ^ 2 = (m : ℤ) * x - h) →
      (∀ y ∈ T, g y * (s y : ℤ) ^ 2 = (m : ℤ) * y - h) →
      (∀ x ∈ S, ∀ y ∈ S, |((x - y : ℤ) : ℝ)| ≤ Real.exp L) →
      (∀ x ∈ T, ∀ y ∈ T, |((x - y : ℤ) : ℝ)| ≤ Real.exp L) →
…

Mentions: OAI.Ostmann.PublishedProgressionInput