OAI/NumberTheory/Ostmann/Arithmetic/PrimePairHaarRegularity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.continuous_pageGiantWeight line 10
2. theorem OAI.Ostmann.continuous_correctedPrimePairAverage line 15
3. theorem OAI.Ostmann.correctedPrimePairAverage_norm_le line 25
4. theorem OAI.Ostmann.prime_pair_haar_sum_norm line 56

   Source documentation

   The finite external average may have a different CRT modulus for every assignment. Its pointwise arithmetic bound passes through both giant cells.

   theorem prime_pair_haar_sum_norm {A : Type*} [Fintype A]
       (P : PublishedProgressionInput) (Q : ℕ) (q : A → ℕ) [∀ a, NeZero (q a)]
       (c : A → ℕ → ℕ → ℂ) (H : A → ℝ → ℝ → ℂ)
       (hH : ∀ a, Measurable (Function.uncurry (H a)))
       (K B : A → ℝ) (hK : ∀ a, 0 ≤ K a) (hB : ∀ a, 0 ≤ B a)
       (hbound : ∀ a x y, ‖H a x y‖ ≤ K a)
       (hc : ∀ a, ∀ z : (ZMod (q a))ˣ, ∀ w : (ZMod (q a))ˣ,
         ‖c a (z : ZMod (q a)).val (w : ZMod (q a)).val‖ ≤ B a)
       (u v r s C : ℝ) (hu : 1 ≤ u) (hr : 1 ≤ r)
       (huv : u ≤ v) (hrs : r ≤ s) (hv : v ≤ u + 1) (hs : s ≤ r + 1)
       (hC : 0 ≤ C) (w : A → ℂ)
       (hmean : ∀ x ∈ Set.Ioc u v, ∀ y ∈ Set.Ioc r s,
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput