OAI/NumberTheory/Ostmann/Arithmetic/BulkSignedBoxBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulk_signed_box_bound line 15

   Source documentation

   Summing all boxes with their original harmonic normalization costs only an exponential in the number of slots. The spectator gain is retained.

   theorem bulk_signed_box_bound {I J C : Type*} [Fintype I] [Fintype J] [Fintype C]
       (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))
       (u v : J → C → ℝ) (hu : ∀ j c, 0 < u j c)
       (Z : J → ℝ) (hZ : ∀ j, 0 ≤ Z j)
       (hmass : ∀ j, Z j * ∑ c, ∫ x in Set.Ioc (u j c) (v j c), (x : ℝ)⁻¹ ≤ 2)
       (F : (J → C) → (J → ℝ) → (J → (ZMod r)ˣ) → ℂ)
       (G : ∀ i, (J → (ZMod (p i))ˣ) → ℂ) (A δ : ℝ) (hA : 0 ≤ A) (hδ : 0 ≤ δ)
   …

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