OAI/NumberTheory/Ostmann/Arithmetic/MovingSamplePrimeExpansion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.complexPrimeInterval_sum line 11
2. theorem OAI.Ostmann.complexPrimeInterval_const_mul line 24
3. theorem OAI.Ostmann.complexPrimePair_sum line 33
4. theorem OAI.Ostmann.complexPrimePair_const_mul line 41
5. theorem OAI.Ostmann.movingCompensatedAverage_prime_pair_patterns line 50

   Source documentation

   No prime asymptotic or independence approximation enters this exchange: these are finite sums over the original two giant-prime intervals.

   theorem movingCompensatedAverage_prime_pair_patterns {A : Type*} [Fintype A]
       (μ : ℕ → A → ℝ) (value : A → ℕ) (n : ℕ)
       (H K : ℝ → ℝ → MovingSampleSlots A n → ℂ) (u v r s : ℝ) :
       letI := sampleSetoidFintype (Bool × MovingSampleIndex n)
   …

   Mentions: OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex