PrimeWordInitialStatistic.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The already selected word bin gives the original positive statistic

theorem OAI.Ostmann.prime_word_fixed_bin_statistic line 11

theorem OAI.Ostmann.prime_word_fixed_bin_statistic_norm line 57

Source documentation

The statistic only uses the absolute values of the selected cell means.

theorem prime_word_fixed_bin_statistic_norm {B : Type*}
    (k nc : ℕ) (P : Finset ℕ) (Q : Fin k → Finset ℕ) (R : Fin nc → Finset ℕ)
    (hQ : ∀ i, Q i ⊆ P) (hR : ∀ i, R i ⊆ P)
    (hQmass : ∀ i, (∑ p ∈ Q i, (p : ℝ)⁻¹) ≠ 0)
    (hRmass : ∀ i, (∑ p ∈ R i, (p : ℝ)⁻¹) ≠ 0)
    (χ : ∀ p : ℕ, DirichletCharacter ℂ p) (t : ∀ p : ℕ, ZMod p)
    (E : Finset ℤ) (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (hX : 0 < X)
    (bin : (Fin k → P) → B) (b : B) (c ρ γ : ℝ)
    (hρ : 0 ≤ ρ) (hγ : 0 ≤ γ)
    (hψ : ∀ x, 0 ≤ (ψ x).re) (hreal : ∀ x, (ψ x).im = 0)
    (hcE : ∀ a ∈ E, c ≤ (ψ ((a : ℝ) / X)).re)
    (hword : ∀ a ∈ E, ρ ≤ ‖binnedWordAverage (fun i => primeSubsetPrior P (Q i))
…

Mentions: OAI.Ostmann.binnedWordAverage, OAI.Ostmann.primeSubsetPrior