OAI/NumberTheory/Ostmann/Arithmetic/PrimePatternFrequencyNormSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Summing two-prime arithmetic coefficients with their actual pattern cost

  1. theorem OAI.Ostmann.prime_pattern_frequency_norm_sum_le line 13

    Source documentation

    The same retained frequency sum survives summing every equality pattern of the original internal prime samples.

    theorem prime_pattern_frequency_norm_sum_le (S : Finset ℤ) (n N V : ℕ)
    (D E K err : ℝ) (hD : 0 ≤ D) (hE : 0 ≤ E) (hK : 0 ≤ K) (herr : 0 ≤ err)
    (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N)
    (hdiv : ∀ q : ℕ, q ≠ 0 → q ≤ N ^ 2 → (q.divisors.card : ℝ) ≤ D) :
    let _ := sampleSetoidFintype (Bool × MovingSampleIndex n)
…

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