PrimeProductGcdError.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Removing GCD restrictions on two independent selected prime products

The probability of a common selected prime is bounded by the sum of the products of the two marginal hit probabilities. For the independent 1/(2p) selection laws this is at most 1/(4N) when all allowed primes exceed N. The same bound controls any bounded test of the selected pair.

def OAI.JointDickman.primeSubsetPairMass line 21
theorem OAI.JointDickman.primeSubsetPairMass_nonneg line 25
theorem OAI.JointDickman.bernoulliSubsetMass_single_hit line 32
theorem OAI.JointDickman.primeSubsetPairMass_common_hit line 39
theorem OAI.JointDickman.primeProducts_coprime_iff_disjoint line 55

theorem OAI.JointDickman.primeSubsetPairMass_gcd_error line 73

Source documentation

A genuine finite union bound for the failure of endpoint coprimality.

theorem primeSubsetPairMass_gcd_error (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (q r : ℕ → ℝ) (hq : ∀ p ∈ P, 0 ≤ q p ∧ q p ≤ 1)
    (hr : ∀ p ∈ P, 0 ≤ r p ∧ r p ≤ 1) :
    finiteProbability (primeSubsetPairMass P q r)
      (fun x => ¬(∏ p ∈ x.1.val, p).Coprime (∏ p ∈ x.2.val, p)) ≤
        ∑ p ∈ P, q p * r p := by
…

Mentions: OAI.JointDickman.finiteProbability, OAI.JointDickman.primeSubsetPairMass

theorem OAI.JointDickman.halfPrimeSelection_bounds line 95

theorem OAI.JointDickman.halfPrimeSubsetPair_gcd_error line 106

Source documentation

The two independent selected products have the manuscript's 1/(2p) law. Their common-prime probability is at most 1/(4N).

theorem halfPrimeSubsetPair_gcd_error (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    {N : ℕ} (hN : N ≠ 0) (hcut : ∀ p ∈ P, N < p) :
    finiteProbability (primeSubsetPairMass P (fun p => (1 / 2 : ℝ) / p)
      (fun p => (1 / 2 : ℝ) / p))
      (fun x => ¬(∏ p ∈ x.1.val, p).Coprime (∏ p ∈ x.2.val, p)) ≤ 1 / (4 * N : ℝ) := by
…

Mentions: OAI.JointDickman.finiteProbability, OAI.JointDickman.primeSubsetPairMass

theorem OAI.JointDickman.primeSubsetPair_coprime_test_error line 126

Source documentation

Inserting or removing endpoint coprimality in a bounded complex test costs at most its bound times the common-prime probability.

theorem primeSubsetPair_coprime_test_error (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (q r : ℕ → ℝ) (hq : ∀ p ∈ P, 0 ≤ q p ∧ q p ≤ 1)
    (hr : ∀ p ∈ P, 0 ≤ r p ∧ r p ≤ 1)
    (F : P.powerset × P.powerset → ℂ) {L : ℝ} (hL : 0 ≤ L) (hF : ∀ x, ‖F x‖ ≤ L) :
    ‖(∑ x, (primeSubsetPairMass P q r x : ℂ) * F x) -
      (∑ x, if (∏ p ∈ x.1.val, p).Coprime (∏ p ∈ x.2.val, p) then
        (primeSubsetPairMass P q r x : ℂ) * F x else 0)‖ ≤ L * ∑ p ∈ P, q p * r p := by
…

Mentions: OAI.JointDickman.primeSubsetPairMass

theorem OAI.JointDickman.halfPrimeSubsetPair_coprime_test_error line 161
theorem OAI.JointDickman.real_restriction_error_of_complex line 180

theorem OAI.JointDickman.halfPrimeSubsetPair_coprime_test_error_real line 203

Source documentation

The same removal estimate for real arithmetic weights.

theorem halfPrimeSubsetPair_coprime_test_error_real (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    {N : ℕ} (hN : N ≠ 0) (hcut : ∀ p ∈ P, N < p)
    (F : P.powerset × P.powerset → ℝ) {L : ℝ} (hL : 0 ≤ L) (hF : ∀ x, |F x| ≤ L) :
    |(∑ x, primeSubsetPairMass P (fun p => (1 / 2 : ℝ) / p)
        (fun p => (1 / 2 : ℝ) / p) x * F x) -
      (∑ x, if (∏ p ∈ x.1.val, p).Coprime (∏ p ∈ x.2.val, p) then
        primeSubsetPairMass P (fun p => (1 / 2 : ℝ) / p)
          (fun p => (1 / 2 : ℝ) / p) x * F x else 0)| ≤ L / (4 * N : ℝ) := by
…

Mentions: OAI.JointDickman.primeSubsetPairMass

theorem OAI.JointDickman.additive_triple_coprime_iff line 217
Source documentation
If the two endpoints are coprime, the additive coefficient is coprime to each endpoint as well. This does not require a restriction on the lag.
```
theorem additive_triple_coprime_iff {a b c j : ℕ} (heq : a = b + j * c) :
    a.Coprime b ∧ a.Coprime c ∧ b.Coprime c ↔ a.Coprime b := by
…
```
theorem OAI.JointDickman.additive_triple_coprime_iff_int_sub line 230