OAI/NumberTheory/TwoPoint/Bounds/PaddingResidueEvent.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Padding divisibility in one common residue sample, with arbitrary departures.

  1. def OAI.TwoPointCorrelations.paddingPrimeSupport line 12
  2. def OAI.TwoPointCorrelations.PaddingResidueEvent line 15
  3. theorem OAI.TwoPointCorrelations.paddingResidueEvent_probability_le line 22

    Source documentation

    Repeated padding primes impose compatibility conditions on a single coordinate. The probability pays only one reciprocal per distinct prime.

    theorem paddingResidueEvent_probability_le {R : ℕ} (Q : Finset ℕ)
    (q : Fin R → ℕ) (offset : Fin R → ℤ) (B : ℕ)
    (hp : ∀ p ∈ Q, 0 < p) (hpB : ∀ p ∈ Q, p ≤ B)
    (hQ : paddingPrimeSupport q ⊆ Q) :
    (FiniteLaw.independent (fun p : Q =>
      uniformResidueLaw B p.val (hp _ p.property) (hpB _ p.property))).probability
        (PaddingResidueEvent Q q offset) ≤
      ∏ p ∈ paddingPrimeSupport q, (p : ℝ)⁻¹ := by
…

    Mentions: OAI.TwoPointCorrelations.paddingPrimeSupport, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw, OAI.TwoPointCorrelations.PaddingResidueEvent