OAI/NumberTheory/Ostmann/Arithmetic/BulkResidueAbsolute.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.uniform_equiv_product_average_real line 11
2. theorem OAI.Ostmann.bulk_residue_absolute_mean_le line 25

   Source documentation

   Page factors at every original bulk slot cost at most two. The frequency and spectator averages still retain their independent CRT coordinates.

   theorem bulk_residue_absolute_mean_le {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 : ℕ) (Y : J → ℝ) (hY : ∀ j, 0 ≤ Y j)
       (F : (J → (ZMod r)ˣ) → ℂ) (G : ∀ i, (J → (ZMod (p i))ˣ) → ℂ)
       (B : ℝ) (hB : 0 ≤ B) (C : I → ℝ)
       (hF : (Fintype.card (J → (ZMod r)ˣ) : ℝ)⁻¹ * ∑ a, ‖F a‖ ≤ B)
       (hG : ∀ i, (Fintype.card (J → (ZMod (p i))ˣ) : ℝ)⁻¹ * ∑ a, ‖G i a‖ ≤ C i) :
       (Fintype.card (J → (ZMod (∏ i, bulkResidueModuli r p i))ˣ) : ℝ)⁻¹ *
         (∑ x : J → (ZMod (∏ i, bulkResidueModuli r p i))ˣ,
           ‖(F (bulkResidueEquiv r p hc x).1 *
   …

   Mentions: OAI.Ostmann.bulkResidueModuli, OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.bulkResidueEquiv