theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPrime_totient_weighted_correction (s : Finset ℕ) (w : ℕ → ℝ) (hs : ∀ p ∈ s, Nat.Prime p) : ∑ p ∈ s, w p / ↑p.totient = ∑ p ∈ s, w p / ↑p + ∑ p ∈ s, w p / (↑p * (↑p - 1))

The omitted term in replacing 1/phi(p) by 1/p is retained exactly. Weights need not be positive for this identity.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPrime_totient_weighted_le (s : Finset ℕ) (w : ℕ → ℝ) (Z : ℝ) (hZ : 1 < Z) (hs : ∀ p ∈ s, Nat.Prime p ∧ Z ≤ ↑p) (hw : ∀ p ∈ s, 0 ≤ w p) : ∑ p ∈ s, w p / ↑p.totient ≤ (1 + 1 / (Z - 1)) * ∑ p ∈ s, w p / ↑p

Uniform relative payment of the positive correction, valid for every nonnegative weight on the actual finite set of primes above Z.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPrime_totient_weighted_rpow_eventually (α η : ℝ) (hα : 0 < α) (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (s : Finset ℕ) (w : ℕ → ℝ), (∀ p ∈ s, Nat.Prime p ∧ ↑N ^ α ≤ ↑p) → (∀ p ∈ s, 0 ≤ w p) → ∑ p ∈ s, w p / ↑p.totient ≤ (1 + η) * ∑ p ∈ s, w p / ↑p

The N threshold is chosen before the finite prime set and its weights; therefore it applies to kernels and supports varying with N.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3PrimeWeights_totient_upper_eventually (α η : ℝ) (hα : 0 < α) (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (y : ℝ) (w : ℕ → ℝ), (∀ p ∈ goldbachClosedPrimes N (↑N ^ α) y, 0 ≤ w p) → ∑ p ∈ goldbachClosedPrimes N (↑N ^ α) y, w p / ↑p.totient ≤ (1 + η) * ∑ p ∈ goldbachClosedPrimes N (↑N ^ α) y, w p / ↑p

Specialization to the actual closed S3 outer prime carrier, uniformly in its upper endpoint and in the nonnegative kernel.