WeightedRegularNorm.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The regular-transform norm under the actual prime sampling law

theorem OAI.Ostmann.weightedPageIntegral_le line 13

theorem OAI.Ostmann.PublishedProgressionInput.actual_regular_prime_norm_le line 39

Source documentation

The exact CRT test mass turns per-residue prime progression errors into an averaged regular-transform bound. The prime sampling weights and the retained exceptional term are both explicit in this statement.

theorem PublishedProgressionInput.actual_regular_prime_norm_le
    (P : PublishedProgressionInput) {I : Type*} [Fintype I] [DecidableEq I]
    (p : I → ℕ) [∀ i, Fact (p i).Prime] [NeZero (∏ i, p i)]
    (hc : Pairwise (fun i j => (p i).Coprime (p j)))
    (a : ∀ i, (ZMod (p i))ˣ) (g : ∀ i, ZMod (p i) → ℂ)
    (hg : ∀ i, g i 0 = 0) (henergy : ∀ i, (∑ x : ZMod (p i), ‖g i x‖ ^ 2) = p i)
    (Q : ℕ) (hQ : 2 ≤ Q) (hmod : (∏ i, p i) ≤ Q)
    {s t : ℝ} (hs : 1 ≤ s) (hst : s ≤ t) (hshort : t ≤ s + 1)
    (w : ℝ → ℝ) (hwc : ContinuousOn w (Set.Icc s t))
    (hw : ∀ y ∈ Set.Ioc s t, 0 ≤ w y)
    (w₀ η Z : ℝ) (hη : 0 ≤ η) (hZ : 0 ≤ Z)
    (hvar : ∀ y ∈ Set.Ioc s t, |w y - w₀| ≤ η) :
…

Mentions: OAI.Ostmann.PublishedProgressionInput