NoChangeSplitBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The no-change part of the amplification second moment

theorem OAI.JointDickman.highPrimePart_at_cutoff line 12
def OAI.JointDickman.noChangeSplitMass line 23
Source documentation
All second assignments agree with the first assignments, retaining the necessary lower tail restrictions on the two remaining sets.
```
noncomputable def noChangeSplitMass (B : ℕ) (A D : Finset ℕ) (C : ℝ) : ℝ :=
…
```
theorem OAI.JointDickman.regular_no_change_split_bound line 29

theorem OAI.JointDickman.regular_no_change_vanishing line 62

Source documentation

Uniform vanishing after the extra factor B needed in the second moment.

theorem regular_no_change_vanishing (L : ℕ) (τ C : ℝ) :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ B : ℕ in atTop, ∀ A D : Finset ℕ,
      A ⊆ auxiliaryPrimes B → D ⊆ auxiliaryPrimes B →
      RegularPrimeSet B L τ C A → RegularPrimeSet B L τ C D →
      (B : ℝ) * noChangeSplitMass B A D C ≤ ε := by
…

Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.noChangeSplitMass