OAI/NumberTheory/Ostmann/ZeroDensity/BulkAbsoluteDensity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulk_absolute_density_crt line 13

   Source documentation

   The absolute coefficient also separates exactly by CRT. In particular, the frequency indicators are kept inside their original Haar average.

   theorem bulk_absolute_density_crt {I J : Type*} [Fintype I] [Fintype J]
       (r : ℕ) [NeZero r] (p : I → ℕ) [∀ i, NeZero (p i)]
       [NeZero (∏ i, bulkResidueModuli r p i)]
       (hc : Pairwise (fun i j => (bulkResidueModuli r p i).Coprime (bulkResidueModuli r p j)))
       (P : PublishedProgressionInput) (Q : ℕ)
       (hpage : pageAtModulus (∏ i, bulkResidueModuli r p i) (selectedPageZero P Q) =
         pageAtModulus r (selectedPageZero P Q))
       (y : J → ℝ) (F : (J → (ZMod r)ˣ) → ℂ)
       (G : ∀ i, (J → (ZMod (p i))ˣ) → ℂ) :
       (∑ z, ‖F (bulkResidueEquiv r p hc z).1 * ∏ i, G i ((bulkResidueEquiv r p hc z).2 i)‖ *
         ∏ j, selectedPrimeLogDensity P Q (∏ i, bulkResidueModuli r p i) (z j).val.val (y j)) =
       (((Fintype.card (J → (ZMod r)ˣ) : ℝ)⁻¹ *
   …

   Mentions: OAI.Ostmann.bulkResidueModuli, OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.pageAtModulus, OAI.Ostmann.selectedPageZero, OAI.Ostmann.bulkResidueEquiv, OAI.Ostmann.selectedPrimeLogDensity

2. theorem OAI.Ostmann.bulk_absolute_density_le line 37