FiniteSieveMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite product mass and its first logarithmic moment for the Selberg denominator.

lemma OAI.TotientAsymptotic.subset_weight_moment line 10

lemma OAI.TotientAsymptotic.subset_weight_below_half line 37

Source documentation

If the first moment is at most half the cutoff, at least half of the Euler-product mass comes from subsets below that cutoff.

lemma subset_weight_below_half (S : Finset ℕ) (w l : ℕ → ℝ)
    (hw : ∀ p ∈ S,0 ≤ w p) (hl : ∀ p ∈ S,0 ≤ l p)
    {L : ℝ} (hL : 0 < L)
    (hmean : (∑ p ∈ S,w p*l p/(1+w p)) ≤ L/2) :
    (∏ p ∈ S,(1+w p))/2 ≤
      ∑ T ∈ S.powerset,if (∑ p ∈ T,l p) ≤ L then (∏ p ∈ T,w p) else 0 := by
…

Mentions: OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.L