ReciprocalSampling.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal-weighted prime sampling and concrete triangular relation bounds.

theorem OAI.TwoPointCorrelations.FiniteLaw.reciprocal_probability_bound line 19

Source documentation

A reciprocal atom majorant transfers the finite progression bound to sampling probability. For the normalized law 1/(Vp), it suffices that V ≥ 1, exactly as in the singleton argument.

theorem reciprocal_probability_bound (μ : FiniteLaw A) (value : A → ℕ)
    (hinj : Function.Injective value) (H N p : ℕ) (C D : ℤ)
    (hH : 0 < H) (hN : 1 ≤ N) (hp : p.Prime) (hC : ¬(p : ℤ) ∣ C)
    (hlo : ∀ a, H ≤ value a) (hhi : ∀ a, value a ≤ N)
    (hweight : ∀ a, μ.weight a ≤ (value a : ℝ)⁻¹)
    (E : A → Prop) (hE : ∀ a, E a → (p : ℤ) ∣ C * value a + D) :
    μ.probability E ≤ (H : ℝ)⁻¹ + (1 + Real.log N) / p := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw

theorem OAI.TwoPointCorrelations.FiniteLaw.nondegenerate_reciprocal_probability_bound line 50

Source documentation

Retain the coefficient test during summation. A vanishing coefficient makes the event empty and costs zero, so no case is lost by resampling.

theorem nondegenerate_reciprocal_probability_bound (μ : FiniteLaw A) (value : A → ℕ)
    (hinj : Function.Injective value) (H N p : ℕ) (C D : ℤ)
    (hH : 0 < H) (hN : 1 ≤ N) (hp : p.Prime)
    (hlo : ∀ a, H ≤ value a) (hhi : ∀ a, value a ≤ N)
    (hweight : ∀ a, μ.weight a ≤ (value a : ℝ)⁻¹) :
    μ.probability (fun a => (p : ℤ) ∣ C * value a + D ∧ ¬(p : ℤ) ∣ C) ≤
      (H : ℝ)⁻¹ + (1 + Real.log N) / p := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw

def OAI.TwoPointCorrelations.integerPrimeAssignment line 70
lemma OAI.TwoPointCorrelations.integerPrimeAssignment_update line 72

lemma OAI.TwoPointCorrelations.primeRelationEvent_update_selected line 80

Source documentation

At a selected coordinate, the concrete monomial event is precisely a single nondegenerate linear congruence with all remaining variables fixed.

lemma primeRelationEvent_update_selected {τ : Type*} [Fintype τ]
    (m : τ → PrimeMonomial ι) (selected control : ι) (hne : control ≠ selected)
    (value : A → ℕ) (x : ι → A) (a : A) :
    primeRelationEvent m selected control
        (integerPrimeAssignment value (Function.update x selected a)) ↔
      (value (x control) : ℤ) ∣
          primeRelationCoefficient m selected (integerPrimeAssignment value x) * value a +
          primeRelationConstant m selected (integerPrimeAssignment value x) ∧
        ¬(value (x control) : ℤ) ∣
          primeRelationCoefficient m selected (integerPrimeAssignment value x) := by
…

Mentions: OAI.TwoPointCorrelations.PrimeMonomial, OAI.TwoPointCorrelations.primeRelationEvent, OAI.TwoPointCorrelations.integerPrimeAssignment, OAI.TwoPointCorrelations.primeRelationCoefficient, OAI.TwoPointCorrelations.primeRelationConstant

lemma OAI.TwoPointCorrelations.primeRelationEvent_update_irrelevant line 99

Source documentation

The pointwise support exclusion proved for the witness ordering is the exact update invariance required by finite triangular elimination.

lemma primeRelationEvent_update_irrelevant {τ : Type*} [Fintype τ]
    (m : τ → PrimeMonomial ι) (selected control j : ι)
    (value : A → ℕ) (x : ι → A) (a : A)
    (hj : j ∉ primeRelationSupport m) (hjc : control ≠ j) :
    primeRelationEvent m selected control (integerPrimeAssignment value (Function.update x j a)) ↔
      primeRelationEvent m selected control (integerPrimeAssignment value x) := by
…

Mentions: OAI.TwoPointCorrelations.PrimeMonomial, OAI.TwoPointCorrelations.primeRelationSupport, OAI.TwoPointCorrelations.primeRelationEvent, OAI.TwoPointCorrelations.integerPrimeAssignment

theorem OAI.TwoPointCorrelations.FiniteLaw.triangular_prime_relation_probability line 113

Source documentation

Fully finite singleton saving for an explicitly triangular family of prime-monomial relations. Later variables occur neither in earlier relations nor in their controlling primes.

theorem triangular_prime_relation_probability {τ : Type*} [Fintype τ]
    [Fintype ι] [LinearOrder ι] [Fintype A] [Nonempty A]
    (μ : ι → 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 : ℝ)⁻¹)
    (m : ι → τ → PrimeMonomial ι) (control : ι → ι)
    (R : Finset ι)
    (hcontrol : ∀ i ∈ R, control i ≠ i)
    (htriangular : ∀ i ∈ R, ∀ j ∈ R, i < j →
      j ∉ primeRelationSupport (m i) ∧ control i ≠ j) :
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.PrimeMonomial, OAI.TwoPointCorrelations.primeRelationSupport