OriginalPrimeRestoration.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Restoring the exceptional atoms inside the original prime expectation

theorem OAI.Ostmann.BulkIntegrand.originalPrimePriors_mean line 12

theorem OAI.Ostmann.BulkIntegrand.averages_primeRestoration line 26

Source documentation

The original normalization is unchanged when the omitted atoms are restored. Only their harmonic mass enters the simultaneous error.

theorem BulkIntegrand.averages_primeRestoration {σ : Type*} [Fintype σ]
    (f : BulkIntegrand σ) (S D : σ → Finset ℕ)
    (hS : ∀ i, (∑ p ∈ S i \ D i, (p : ℝ)⁻¹) ≠ 0)
    (order : List σ) (horder : order.Nodup)
    (C : ℝ) (hC : 0 ≤ C) (hf : ∀ x, ‖f x‖ ≤ C)
    (hsmall : ∀ i ∈ order,
      (∑ p ∈ S i \ D i, (p : ℝ)⁻¹)⁻¹ * ∑ p ∈ S i ∩ D i, (p : ℝ)⁻¹ ≤ 1) :
    let Z := fun i => (∑ p ∈ S i \ D i, (p : ℝ)⁻¹)⁻¹
…

Mentions: OAI.Ostmann.BulkIntegrand

theorem OAI.Ostmann.BulkIntegrand.originalPrimePriors_restoration line 54

Source documentation

Apply the exceptional-atom restoration under the full original law, including every nonbulk coordinate.

theorem BulkIntegrand.originalPrimePriors_restoration {σ : Type*} [Fintype σ]
    (f : BulkIntegrand σ) (P : Finset ℕ) (S D : σ → Finset ℕ)
    (hSP : ∀ i, S i \ D i ⊆ P)
    (hS : ∀ i, (∑ p ∈ S i \ D i, (p : ℝ)⁻¹) ≠ 0)
    (order : List σ) (horder : order.Nodup)
    (C : ℝ) (hC : 0 ≤ C) (hf : ∀ x, ‖f x‖ ≤ C)
    (hsmall : ∀ i ∈ order,
      (∑ p ∈ S i \ D i, (p : ℝ)⁻¹)⁻¹ * ∑ p ∈ S i ∩ D i, (p : ℝ)⁻¹ ≤ 1) :
    let Z := fun i => (∑ p ∈ S i \ D i, (p : ℝ)⁻¹)⁻¹
…

Mentions: OAI.Ostmann.BulkIntegrand