OAI/NumberTheory/TwoPoint/Bounds/PositiveRowMajorant.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The literal sum of positive tuple weights is the row majorant whose second moment was estimated under the product law.

  1. lemma OAI.TwoPointCorrelations.positivePrimeWeight_tuple line 15
  2. lemma OAI.TwoPointCorrelations.positivePrimeWeight_tuple_sum line 30
  3. lemma OAI.TwoPointCorrelations.positivePrimeWeight_tuple_sum_le line 47
  4. lemma OAI.TwoPointCorrelations.abs_centeredTuple_sum_le line 66

    Source documentation

    The deterministic first-power bound needed when testing the graph against bounded vectors. The degree projection is the only site restriction.

    lemma abs_centeredTuple_sum_le {J : ℕ} (P : Fin J → Finset ℕ)
    (hprime : ∀ j, ∀ p ∈ P j, p.Prime)
    (hdisjoint : ∀ j l, l ≠ j → Disjoint (P j) (P l)) (n : ℤ) (W : ℝ)
    (hV : ∀ j, primeHarmonicMass (P j) ≤ 2 * W)
    (hdegree : (actualPaddingDegree (univ.biUnion P) n : ℝ) ≤ 6 * W * J) :
    (∑ d ∈ primeTupleDivisors P, |centeredTuple d.primeFactors n|) ≤ (8 * W) ^ J := by
…

    Mentions: OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.actualPaddingDegree, OAI.TwoPointCorrelations.primeTupleDivisors, OAI.TwoPointCorrelations.centeredTuple

  5. lemma OAI.TwoPointCorrelations.positive_tuple_padding_row_bound line 75