ShiftedSieveDenominator.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A finite Euler-product lower bound for the concrete Selberg denominator.

def OAI.TotientAsymptotic.shiftedSieveWeight line 13
lemma OAI.TotientAsymptotic.shiftedSieveWeight_nonneg line 16
lemma OAI.TotientAsymptotic.shiftedSieveWeight_moment line 22
lemma OAI.TotientAsymptotic.shiftedSieve_moment_le line 35
lemma OAI.TotientAsymptotic.shiftedSieveTerms_prod line 62
lemma OAI.TotientAsymptotic.shiftedSieveBoundingSum_powerset line 76
theorem OAI.TotientAsymptotic.shiftedSieveBoundingSum_lower line 98
Source documentation
The logarithmic first moment confines at least half of the Euler product to integers within the square-root cutoff used by Selberg's denominator.
```
theorem shiftedSieveBoundingSum_lower (b X z : ℕ) (y : ℝ) (hy : 1 < y)
    (hz : 2 ≤ z) (hscale : 8*Real.log 4*(2+Real.log z) ≤ Real.log y) :
    (∏ p ∈ oddSievePrimes z,(1+shiftedSieveWeight b p))/2 ≤
      selbergBoundingSum (shiftedPrimeSieve b X z y hy.le) := by
…
```
Mentions: OAI.TotientAsymptotic.oddSievePrimes, OAI.TotientAsymptotic.shiftedSieveWeight, OAI.TotientAsymptotic.shiftedPrimeSieve