Euler and absolute bounds for the same truncated signed family

The tail includes primes equal to the truncation point. The absolute estimate uses the actual squarefree aggregate, not the sum of magnitudes of its labels.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.EdgeDensity.euler_truncation_ratio (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {g : ℕ → ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) {w z K : ℝ} (hw : 2 ≤ w) (hwz : w < z) (hcut : ∀ p ∈ P, ↑p < z) (hdim : SmallRosser.DimensionOneProductBound P g K) : (∏ p ∈ P with ↑p < w, (1 - g p)) / ∏ p ∈ P, (1 - g p) ≤ Real.log z / Real.log w * (1 + K / Real.log w)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.EdgeDensity.signedFamilyDensity_abs_le_plusProduct (upper : Bool) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hcut : ∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < √D) {g : ArithmeticFunction ℝ} (hgm : g.IsMultiplicative) (hg : ∀ p ∈ P, 0 ≤ g p) : |signedFamilyDensity upper P D ε (geometricSieveLabel D ε) g| ≤ ∏ p ∈ P, (1 + g p)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.EdgeDensity.plusProduct_le_full_euler (P B : Finset ℕ) (hBP : B ⊆ P) (hP : ∀ p ∈ P, Nat.Prime p) {g : ℕ → ℝ} (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) {z K : ℝ} (hz : 2 < z) (hcut : ∀ p ∈ P, ↑p < z) (hdim : SmallRosser.DimensionOneProductBound P g K) : ∏ p ∈ B, (1 + g p) ≤ (∏ p ∈ P, (1 - g p)) * (Real.log z / Real.log 2 * (1 + K / Real.log 2)) ^ 2