RegularResidueNorm.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Averaged regular-transform norm on the actual CRT residue classes

The sum of the nonnegative residue test is the squarefree modulus itself. Consequently the progression errors are summed against its exact mass, with no pointwise estimate on the small-prime transforms.

theorem OAI.Ostmann.sum_regular_local_norm line 17
def OAI.Ostmann.regularResidueTest line 26
theorem OAI.Ostmann.regularResidueTest_nonneg line 32

theorem OAI.Ostmann.sum_regularResidueTest line 39

Source documentation

Exact normalization (the manuscript's CRT norm identity).

theorem sum_regularResidueTest {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) :
    (∑ u, regularResidueTest p hc a g u) = (∏ i, p i : ℕ) := by
…

Mentions: OAI.Ostmann.regularResidueTest

theorem OAI.Ostmann.positive_test_progression_bound line 59

Source documentation

A positive residue test can be summed against per-class progression errors at the cost of its exact total mass.

theorem positive_test_progression_bound {A : Type*} [Fintype A]
    (μ ν F : A → ℝ) (δ K : ℝ) (hF : ∀ a, 0 ≤ F a)
    (hdist : ∀ a, |μ a - ν a| ≤ δ) (hν : ∀ a, ν a ≤ K) :
    (∑ a, μ a * F a) ≤ (K + δ) * ∑ a, F a := by
…

theorem OAI.Ostmann.regular_prime_residue_norm_le line 70

Source documentation

The regular transform estimate keeps any Page correction in ν; only its pointwise factor-two bound is used here.

theorem regular_prime_residue_norm_le {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)
    (μ ν : (ZMod (∏ i, p i))ˣ → ℝ) (δ R : ℝ)
    (hdist : ∀ u, |μ u - ν u| ≤ δ)
    (hν : ∀ u, ν u ≤ 2 * R / Fintype.card (ZMod (∏ i, p i))ˣ) :
    (∑ u, μ u * regularResidueTest p hc a g u) ≤
      (2 * R / Fintype.card (ZMod (∏ i, p i))ˣ + δ) * (∏ i, p i : ℕ) := by
…

Mentions: OAI.Ostmann.regularResidueTest

theorem OAI.Ostmann.totient_factor_le_exp line 85

theorem OAI.Ostmann.regular_unit_ratio_le_exp line 98

Source documentation

The CRT unit-density correction is close to one when all slot primes are large compared with their number.

theorem regular_unit_ratio_le_exp {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)))
    (Z : ℝ) (hZ : 2 ≤ Z) (hpZ : ∀ i, Z ≤ p i) :
    ((∏ i, p i : ℕ) : ℝ) / Fintype.card (ZMod (∏ i, p i))ˣ ≤
      Real.exp (2 * Fintype.card I / Z) := by
…