HarmonicRepeatRemoval.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Removing repeated primes from an original-prior character statistic

theorem OAI.Ostmann.harmonic_repeat_removal line 14

Source documentation

The event S contains the original bin and product restrictions. Its harmonic law is never renormalized when repeated primes are removed.

theorem harmonic_repeat_removal (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (n : ℕ) (Q : Fin n → Finset ℕ) (S : Finset (Fin n → P))
    (χ : Fin n → ∀ p : ℕ, DirichletCharacter ℂ p)
    (hχ : ∀ i p, p ∈ P → χ i p ≠ 1) (t : ∀ p : ℕ, ZMod p)
    (ψ : 𝓢(ℝ, ℂ)) (X H R D : ℝ) (hX : 0 < X) (hR : 0 < R)
    (hsupp : ∀ x : ℝ, H < |x| → 𝓕 ψ x = 0)
    (hsmall : ∀ p ∈ P, H * R < p)
    (hupper : ∀ x ∈ S, (∏ i, (x i : ℝ)) ≤ X * R)
    (hlower : ∀ x ∈ S, X * Real.exp D ≤ ∏ i, (x i : ℝ)) :
    let μ := fun i => primeSubsetPrior P (Q i)
…

Mentions: OAI.Ostmann.primeSubsetPrior