InfiniteSplitMass.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Passing the prime-series bounds to a finite set of split primes

def OAI.Ostmann.retainedSplitTerm line 14
def OAI.Ostmann.divisorPrimeTerm line 17
theorem OAI.Ostmann.retainedSplitTerm_support line 20
theorem OAI.Ostmann.retainedSplitTerm_summable line 27
theorem OAI.Ostmann.retainedSplitTerm_tsum line 31
theorem OAI.Ostmann.divisorPrimeTerm_support line 41
theorem OAI.Ostmann.divisorPrimeTerm_summable line 48
theorem OAI.Ostmann.divisorPrimeTerm_mass line 52
theorem OAI.Ostmann.split_prime_pointwise line 68
Source documentation
This is the pointwise split-prime identity, with explicit losses for large primes and divisors of the excluded integer.
```
theorem split_prime_pointwise (d : ℤ) (D Q : ℕ) (s : ℝ) (hdD : d.natAbs ∣ D) (n : ℕ) :
    unsignedPrimeTerm s n + jacobiPrimeTerm d s n ≤
      2 * retainedSplitTerm d D Q s n + 2 * unsignedPrimeTail Q s n + 2 * divisorPrimeTerm D s n := by
…
```
Mentions: OAI.Ostmann.unsignedPrimeTerm, OAI.Ostmann.jacobiPrimeTerm, OAI.Ostmann.retainedSplitTerm, OAI.Ostmann.unsignedPrimeTail, OAI.Ostmann.divisorPrimeTerm

theorem OAI.Ostmann.retained_split_mass_from_series line 98

Source documentation

Infinite unsigned and signed series give a lower bound for the actual finite retained set; all excluded-divisor weights are bounded explicitly.

theorem retained_split_mass_from_series (d : ℤ) (D Q Y : ℕ) (s L B T : ℝ)
    (hdD : d.natAbs ∣ D) (hD : 0 < D) (hY : 0 < Y) (hs : 1 ≤ s)
    (hu : Summable (unsignedPrimeTerm s)) (hj : Summable (jacobiPrimeTerm d s))
    (ht : Summable (unsignedPrimeTail Q s))
    (hL : L ≤ ∑' n, unsignedPrimeTerm s n)
    (hB : -B ≤ ∑' n, jacobiPrimeTerm d s n)
    (hT : (∑' n, unsignedPrimeTail Q s n) ≤ T) :
    (L - B) / 2 - T - (Y + Real.log D / Y) ≤
      ∑ p ∈ (Nat.primesLE Q).filter (fun p => ¬p ∣ D ∧ jacobiSym d p = 1),
        Real.log p / (p : ℝ) ^ s := by
…

Mentions: OAI.Ostmann.unsignedPrimeTerm, OAI.Ostmann.jacobiPrimeTerm, OAI.Ostmann.unsignedPrimeTail