OAI/NumberTheory/Ostmann/Arithmetic/BulkResidueIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.BulkIntegrand.page_density_integrable line 13

   Source documentation

   The full bounded sharp kernel is integrable against the product density.

   theorem BulkIntegrand.page_density_integrable {J : Type*} [Fintype J]
       (f : BulkIntegrand J) (P : PublishedProgressionInput) (Q : ℕ)
       (q a : J → ℕ) (u v : J → ℝ) (hu : ∀ j, 0 < u j) :
       Integrable (fun x => f x * ∏ j, (selectedPrimeLogDensity P Q (q j) (a j) (x j) : ℂ))
         (Measure.pi (fun j => volume.restrict (Set.Ioc (u j) (v j)))) := by
   …

   Mentions: OAI.Ostmann.BulkIntegrand, OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.selectedPrimeLogDensity

2. theorem OAI.Ostmann.bulk_page_residue_integral line 28

   Source documentation

   Residue classes are summed inside the real integral. In particular there is no number-of-boxes factor on the main term.

   theorem bulk_page_residue_integral {J Z : Type*} [Fintype J] [Fintype Z]
       (P : PublishedProgressionInput) (Q : ℕ) (q : J → ℕ) (a : Z → J → ℕ)
       (u v : J → ℝ) (hu : ∀ j, 0 < u j) (f : Z → BulkIntegrand J) :
       (∑ z, ∫ x, f z x ∂Measure.pi (fun j => primeGiantMeasure P Q (q j) (a z j) (u j) (v j))) =
         ∫ x, ∑ z, f z x * ∏ j, (selectedPrimeLogDensity P Q (q j) (a z j) (x j) : ℂ)
           ∂Measure.pi (fun j => volume.restrict (Set.Ioc (u j) (v j))) := by
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.BulkIntegrand, OAI.Ostmann.primeGiantMeasure, OAI.Ostmann.selectedPrimeLogDensity