OrderedPrimeSystems.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A finite ordered family packages the precise output of witness selection.

structure OAI.TwoPointCorrelations.OrderedPrimeSystem line 15
Source documentation
The index order records elimination order; it is unrelated to the names or numerical values of the ambient prime labels.
```
structure OrderedPrimeSystem (ι : Type*) [DecidableEq ι] where
…
```
def OAI.TwoPointCorrelations.OrderedPrimeSystem.size line 35
def OAI.TwoPointCorrelations.OrderedPrimeSystem.Holds line 37

theorem OAI.TwoPointCorrelations.OrderedPrimeSystem.probability_bound line 42

Source documentation

Each selected interval or comparison earns its own factor; every unselected prime variable is averaged with its original product law.

theorem probability_bound [Fintype ι] {A : Type*} [Fintype A] [Nonempty A]
    (S : OrderedPrimeSystem ι) (μ : ι → FiniteLaw A) (value : A → ℕ)
    (hinj : Function.Injective value) (H N : ℕ) (hH : 0 < H) (hN : 1 ≤ N)
    (hprime : ∀ a, (value a).Prime) (hlo : ∀ a, H ≤ value a)
    (hhi : ∀ a, value a ≤ N) (hweight : ∀ i a, (μ i).weight a ≤ (value a : ℝ)⁻¹) :
    (FiniteLaw.independent μ).probability (fun x => S.Holds (integerPrimeAssignment value x)) ≤
      ((H : ℝ)⁻¹ + (1 + Real.log N) / H) ^ S.size := by
…

Mentions: OAI.TwoPointCorrelations.OrderedPrimeSystem, OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.integerPrimeAssignment

theorem OAI.TwoPointCorrelations.OrderedPrimeSystem.reciprocal_sum_bound line 57

Source documentation

The actual reciprocal sum for a fixed recorded system. Keeping the nonzero coefficient tests in Holds makes every elimination valid after resampling, including samples with coincident numerical primes.

theorem reciprocal_sum_bound [Fintype ι] (S : OrderedPrimeSystem ι)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hV : 1 ≤ primeHarmonicMass P)
    (H N : ℕ) (hH : 0 < H) (hN : 1 ≤ N)
    (hlo : ∀ p ∈ P, H ≤ p) (hhi : ∀ p ∈ P, p ≤ N) :
    (∑ x : ι → P, if S.Holds (integerPrimeAssignment Subtype.val x)
      then ∏ z, ((x z).val : ℝ)⁻¹ else 0) ≤
      primeHarmonicMass P ^ Fintype.card ι *
        ((H : ℝ)⁻¹ + (1 + Real.log N) / H) ^ S.size := by
…

Mentions: OAI.TwoPointCorrelations.OrderedPrimeSystem, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.integerPrimeAssignment