OAI/NumberTheory/Ostmann/ZeroDensity/BulkHaarDensity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulk_prime_density_haar line 12

   Source documentation

   Every prime density contributes one Haar-unit normalization and one harmonic factor. Page multipliers remain inside the residue average.

   theorem bulk_prime_density_haar {J : Type*} [Fintype J]
       (P : PublishedProgressionInput) (Q M : ℕ) [NeZero M]
       (y : J → ℝ) (C : (J → (ZMod M)ˣ) → ℂ) :
       (∑ z, C z * ∏ j, (selectedPrimeLogDensity P Q M (z j).val.val (y j) : ℂ)) =
         ((Fintype.card (J → (ZMod M)ˣ) : ℂ)⁻¹ *
           ∑ z, C z * ∏ j, pageGiantWeight P Q M (z j).val.val (y j)) *
             ∏ j, (y j : ℂ)⁻¹ := by
   …

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

2. theorem OAI.Ostmann.bulk_prime_density_crt line 32

   Source documentation

   The full density in the actual product modulus factors into the retained frequency/Page average, independent spectator averages and harmonic densities.

   theorem bulk_prime_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)ˣ) : ℂ)⁻¹ *
           ∑ a, F a * ∏ j, pageGiantWeight P Q r (a j).val.val (y j)) *
   …

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