SplitProjectionSupport.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Projecting a native oriented split event to the low-prime test

theorem OAI.JointDickman.retained_high_projection line 12
theorem OAI.JointDickman.retained_low_high_union line 23
theorem OAI.JointDickman.added_low_projection line 34

theorem OAI.JointDickman.native_oriented_ratio_test line 42

Source documentation

The native size-and-ratio event with an oriented changed prime implies the precise low-addition test used in the conditional small-ball estimate.

theorem native_oriented_ratio_test {B T : ℕ} {Y : ℝ}
    {A D R Q I J U V : Finset ℕ}
    (hB : 0 < B) (hA : A ⊆ auxiliaryPrimes B) (hD : D ⊆ auxiliaryPrimes B)
    (hR : R ⊆ auxiliaryPrimes B) (hQ : Q ⊆ auxiliaryPrimes B)
    (hAR : Disjoint A R) (hDQ : Disjoint D Q)
    (hI : I ⊆ A) (hJ : J ⊆ D) (hU : U ⊆ R) (hV : V ⊆ Q)
    (hnoA : ∀ p ∈ symmDiff A (I ∪ U), Real.log p ≤ Y)
    (hnoD : ∀ p ∈ symmDiff D (J ∪ V), Real.log p ≤ Y)
    (hpair : (∏ p ∈ I ∪ U, p, ∏ p ∈ J ∪ V, p) ∈ amplificationCoefficientPairs B T)
    (hadd : ∃ p ∈ (I ∪ U) \ A, Y / 2 < Real.log p) :
    additionRatioTest Y T
      (∏ p ∈ (I ∩ (A ∩ additionPrimes B Y)) ∪ (A ∩ upperAdditionPrimes B Y), p : ℕ)
…

Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.amplificationCoefficientPairs, OAI.JointDickman.additionRatioTest, OAI.JointDickman.additionPrimes, OAI.JointDickman.upperAdditionPrimes