TripleSieveDenominator.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

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

def OAI.TotientAsymptotic.tripleSieveWeight line 13
lemma OAI.TotientAsymptotic.tripleSieveWeight_nonneg line 16
lemma OAI.TotientAsymptotic.tripleSieveWeight_moment line 22
lemma OAI.TotientAsymptotic.tripleSieve_moment_le line 35
lemma OAI.TotientAsymptotic.tripleSieveTerms_prod line 69
lemma OAI.TotientAsymptotic.tripleSieveBoundingSum_powerset line 83
theorem OAI.TotientAsymptotic.tripleSieveBoundingSum_lower line 105
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 tripleSieveBoundingSum_lower (a b X z : ℕ) (y : ℝ) (hy : 1 < y)
    (hz : 2 ≤ z) (hscale : 12*Real.log 4*(2+Real.log z) ≤ Real.log y) :
    (∏ p ∈ tripleSievePrimes z,(1+tripleSieveWeight a b p))/2 ≤
      selbergBoundingSum (triplePrimeSieve a b X z y hy.le) := by
…
```
Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.tripleSievePrimes, OAI.TotientAsymptotic.tripleSieveWeight, OAI.TotientAsymptotic.triplePrimeSieve