OAI/NumberTheory/Ostmann/Construction/PrimeSubsetLogMeasure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeSubsetLogMeasure line 12
2. instance OAI.Ostmann.finite_primeSubsetLogMeasure line 15
3. theorem OAI.Ostmann.BulkIntegrand.average_primeSubset line 21
4. theorem OAI.Ostmann.BulkIntegrand.average_originalPrimePrior line 39

   Source documentation

   This is the literal original finite prior, with its own normalization; no replacement by a uniformly distributed prime is made.

   theorem BulkIntegrand.average_originalPrimePrior {σ : Type*} [Fintype σ]
       (f : BulkIntegrand σ) (P S : Finset ℕ) (hSP : S ⊆ P) (i : σ) (x : σ → ℝ) :
       f.average (primeSubsetLogMeasure S (∑ p ∈ S, (p : ℝ)⁻¹)⁻¹) i x =
         ∑ p : P, (primeSubsetPrior P S p : ℂ) * f (Function.update x i (Real.log (p : ℕ))) := by
   …

   Mentions: OAI.Ostmann.BulkIntegrand, OAI.Ostmann.primeSubsetLogMeasure, OAI.Ostmann.primeSubsetPrior

5. theorem OAI.Ostmann.BulkIntegrand.primeSubset_deletion_bound line 53

   Source documentation

   Removing the prescribed exceptional primes costs their actual harmonic mass, while retaining the supplied normalization constant.

   theorem BulkIntegrand.primeSubset_deletion_bound {σ : Type*} [Fintype σ]
       (f : BulkIntegrand σ) (S D : Finset ℕ) (Z C : ℝ) (hZ : 0 ≤ Z)
       (hF : ∀ x, ‖f x‖ ≤ C) (i : σ) (x : σ → ℝ) :
       ‖f.average (primeSubsetLogMeasure S Z) i x -
         f.average (primeSubsetLogMeasure (S \ D) Z) i x‖ ≤
           Z * C * ∑ p ∈ S ∩ D, (p : ℝ)⁻¹ := by
   …

   Mentions: OAI.Ostmann.BulkIntegrand, OAI.Ostmann.primeSubsetLogMeasure