theorem G12SharpQuadrature.upper_eventually_eq (u : ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, upper n u = G12SharpWeight.weight u

At each fixed point the continuous upper weights eventually equal the sharp weight.

theorem G12SharpQuadrature.upper_tendsto (u : ℝ) : Filter.Tendsto (fun (n : ℕ) => upper n u) Filter.atTop (nhds (G12SharpWeight.weight u))

theorem G12SharpQuadrature.upper_integral_tendsto : Filter.Tendsto (fun (n : ℕ) => MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral (upper n)) Filter.atTop (nhds (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral G12SharpWeight.weight))

Dominated convergence is applied only to the exact reduced cross integral.

theorem G12SharpQuadrature.sharp_kernel_le_integral_eventually (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel G12SharpWeight.weight N ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral G12SharpWeight.weight + δ

The original discontinuous sharp author weight on the actual four-prime kernel.

theorem G12SharpQuadrature.sharp_kernel_le_split_eventually (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel G12SharpWeight.weight N ≤ Real.log (9 / 4) * ((561990 / 1000000 * (36 / 5) * ∫ (u : ℝ) in 4 / 53..1 / 10, density u / (1 - u)) + 564383 / 1000000 * 8 * ∫ (u : ℝ) in 1 / 10..4 / 33, density u) + δ

Direct one-dimensional low/high consumer, with no numerical bound as an input.