HarmonicUnitPriors.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Harmonic prime residues compared with uniform unit residues

theorem OAI.Ostmann.primeSubsetPrior_unit_residue_le line 14

Source documentation

The factor is the inverse harmonic normalizer times three times the number of dyadic intervals. Boundary primes stay in the original prior.

theorem primeSubsetPrior_unit_residue_le (P S : Finset ℕ) (q h J : ℕ) [NeZero q]
    (hunit : ∀ p : P, (p : ℕ).Coprime q)
    (hsmall : q ≤ 2 ^ h)
    (hrange : ∀ n ∈ S, 2 ^ h ≤ n ∧ n < 2 ^ (h + J)) (a : (ZMod q)ˣ) :
    cellPrior (primeSubsetPrior P S) (fun p => ZMod.unitOfCoprime (p : ℕ) (hunit p)) a ≤
      ((∑ n ∈ S, (n : ℝ)⁻¹)⁻¹ * (3 * J)) * (Fintype.card (ZMod q)ˣ : ℝ)⁻¹ := by
…

Mentions: OAI.Ostmann.cellPrior, OAI.Ostmann.primeSubsetPrior

theorem OAI.Ostmann.harmonic_unit_expectation_le line 46

Source documentation

Nonnegative residue tests may be pulled through the exact pushforward and bounded pointwise by the uniform unit law.

theorem harmonic_unit_expectation_le (P S : Finset ℕ) (q h J : ℕ) [NeZero q]
    (hunit : ∀ p : P, (p : ℕ).Coprime q)
    (hsmall : q ≤ 2 ^ h)
    (hrange : ∀ n ∈ S, 2 ^ h ≤ n ∧ n < 2 ^ (h + J))
    (F : (ZMod q)ˣ → ℝ) (hF : ∀ a, 0 ≤ F a) :
    (∑ p : P, primeSubsetPrior P S p * F (ZMod.unitOfCoprime (p : ℕ) (hunit p))) ≤
      ((∑ n ∈ S, (n : ℝ)⁻¹)⁻¹ * (3 * J)) *
        ((Fintype.card (ZMod q)ˣ : ℝ)⁻¹ * ∑ a, F a) := by
…

Mentions: OAI.Ostmann.primeSubsetPrior