PositiveWordProbability.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Probability of one positive numerical word

The same residue coordinate is reused at every occurrence of a prime. Selecting one occurrence per distinct prime therefore bounds the probability by one reciprocal per distinct prime, including all padding factors. There is no independence assumption between different sites of the word.

lemma OAI.TwoPointCorrelations.FiniteLaw.probability_mono_of_imp line 22
theorem OAI.TwoPointCorrelations.uniformResidueLaw_mod_eq line 34
Source documentation
Every residue modulo the true modulus has precisely its uniform mass, even though the common carrier Fin B also contains zero-weight points.
```
theorem uniformResidueLaw_mod_eq (B p : ℕ) (hp : 0 < p) (hpB : p ≤ B) (r : ZMod p) :
    (uniformResidueLaw B p hp hpB).probability
      (fun x => (x.val : ZMod p) = r) = (p : ℝ)⁻¹ := by
…
```
Mentions: OAI.TwoPointCorrelations.uniformResidueLaw
def OAI.TwoPointCorrelations.wordDivisorPrimeSupport line 67
Source documentation
Distinct prime factors in all the step divisors, both tuples and padding.
```
def wordDivisorPrimeSupport (w : List SignedStep) : Finset ℕ :=
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep
lemma OAI.TwoPointCorrelations.mem_wordDivisorPrimeSupport line 70
def OAI.TwoPointCorrelations.ResiduePositiveWord line 77
Source documentation
Positivity expressed in the one common set of residue coordinates.
```
def ResiduePositiveWord {ι : Type*} (p : ι → ℕ) (h : ℕ) (w : List SignedStep)
    (r : ∀ i, ZMod (p i)) : Prop :=
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep

theorem OAI.TwoPointCorrelations.residuePositiveWord_iff line 84

Source documentation

A residue test is exact arithmetic positivity at any common integer lift.

theorem residuePositiveWord_iff {ι : Type*} (p : ι → ℕ) (h : ℕ)
    (w : List SignedStep) (r : ∀ i, ZMod (p i)) (n : ℤ)
    (hn : ∀ i, (n : ZMod (p i)) = r i)
    (hsq : ∀ a ∈ w, Squarefree (a.padding * a.tuple))
    (hcover : ∀ q ∈ wordDivisorPrimeSupport w, ∃ i, p i = q) :
    ResiduePositiveWord p h w r ↔ PositiveWord h n w := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.wordDivisorPrimeSupport, OAI.TwoPointCorrelations.ResiduePositiveWord, OAI.TwoPointCorrelations.PositiveWord

theorem OAI.TwoPointCorrelations.residuePositiveWord_probability_le line 102

Source documentation

One reciprocal factor for every used residue coordinate. Repeated occurrences can only make the event smaller, by adding compatibility tests.

theorem residuePositiveWord_probability_le {ι : Type*} [Fintype ι] [DecidableEq ι]
    (B : ℕ) (p : ι → ℕ) (hp : ∀ i, 0 < p i) (hpB : ∀ i, p i ≤ B)
    (h : ℕ) (w : List SignedStep) :
    (FiniteLaw.independent (fun i => uniformResidueLaw B (p i) (hp i) (hpB i))).probability
      (fun x => ResiduePositiveWord p h w (fun i => ((x i).val : ZMod (p i)))) ≤
      ∏ i ∈ univ.filter (fun i => p i ∈ wordDivisorPrimeSupport w), (p i : ℝ)⁻¹ := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw, OAI.TwoPointCorrelations.ResiduePositiveWord, OAI.TwoPointCorrelations.wordDivisorPrimeSupport

theorem OAI.TwoPointCorrelations.residuePositiveWord_probability_distinct_primes line 133

Source documentation

For an injectively indexed prime pool covering every step factor, the bound is literally the product over distinct numerical primes in the word.

theorem residuePositiveWord_probability_distinct_primes {ι : Type*}
    [Fintype ι] [DecidableEq ι] (B : ℕ) (p : ι → ℕ)
    (hinj : Function.Injective p) (hp : ∀ i, 0 < p i) (hpB : ∀ i, p i ≤ B)
    (h : ℕ) (w : List SignedStep)
    (hcover : ∀ q ∈ wordDivisorPrimeSupport w, ∃ i, p i = q) :
    (FiniteLaw.independent (fun i => uniformResidueLaw B (p i) (hp i) (hpB i))).probability
      (fun x => ResiduePositiveWord p h w (fun i => ((x i).val : ZMod (p i)))) ≤
      ∏ q ∈ wordDivisorPrimeSupport w, (q : ℝ)⁻¹ := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.wordDivisorPrimeSupport, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw, OAI.TwoPointCorrelations.ResiduePositiveWord

theorem OAI.TwoPointCorrelations.prohibited_residue_catalog_iff line 157

Source documentation

The finite catalog's modular event is exactly the deleted event at any common integer lift. Minimality remains in the catalog, not in the random law.

theorem prohibited_residue_catalog_iff {ι : Type*} (p : ι → ℕ)
    (pairs : Finset (ℕ × ℕ)) (h s : ℕ) (r : ∀ i, ZMod (p i)) (n : ℤ)
    (hn : ∀ i, (n : ZMod (p i)) = r i)
    (hsq : ∀ dq ∈ pairs, Squarefree (dq.2 * dq.1))
    (hcover : ∀ c : ProhibitedCatalog pairs h s,
      ∀ q ∈ wordDivisorPrimeSupport (decodeStepWord c.val), ∃ i, p i = q) :
    (∃ c : ProhibitedCatalog pairs h s, ResiduePositiveWord p h (decodeStepWord c.val) r) ↔
      ProhibitedSite h s (fun d q => (d, q) ∈ pairs) n := by
…

Mentions: OAI.TwoPointCorrelations.ProhibitedCatalog, OAI.TwoPointCorrelations.wordDivisorPrimeSupport, OAI.TwoPointCorrelations.decodeStepWord, OAI.TwoPointCorrelations.ResiduePositiveWord, OAI.TwoPointCorrelations.ProhibitedSite

theorem OAI.TwoPointCorrelations.prohibited_residue_probability_le_catalog line 182

Source documentation

A literal union bound for the actual minimal-word catalog. The remaining arithmetic task is to sum these distinct-prime weights over that catalog.

theorem prohibited_residue_probability_le_catalog {ι : Type*}
    [Fintype ι] [DecidableEq ι] (B : ℕ) (p : ι → ℕ)
    (hinj : Function.Injective p) (hp : ∀ i, 0 < p i) (hpB : ∀ i, p i ≤ B)
    (pairs : Finset (ℕ × ℕ)) (h s : ℕ)
    (hcover : ∀ c : ProhibitedCatalog pairs h s,
      ∀ q ∈ wordDivisorPrimeSupport (decodeStepWord c.val), ∃ i, p i = q) :
    (FiniteLaw.independent (fun i => uniformResidueLaw B (p i) (hp i) (hpB i))).probability
      (fun x => ∃ c : ProhibitedCatalog pairs h s,
        ResiduePositiveWord p h (decodeStepWord c.val)
          (fun i => ((x i).val : ZMod (p i)))) ≤
      ∑ c : ProhibitedCatalog pairs h s,
        ∏ q ∈ wordDivisorPrimeSupport (decodeStepWord c.val), (q : ℝ)⁻¹ := by
…

Mentions: OAI.TwoPointCorrelations.ProhibitedCatalog, OAI.TwoPointCorrelations.wordDivisorPrimeSupport, OAI.TwoPointCorrelations.decodeStepWord, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw, OAI.TwoPointCorrelations.ResiduePositiveWord