noncomputable def G12SharpQuadrature.step (n : ℕ) (u : ℝ) : ℝ

Integer steepness keeps the transition strictly to the left of the junction.

Equations

• G12SharpQuadrature.step n u = min 1 (max 0 (1 + (u - 1 / 10) * ↑n))

noncomputable def G12SharpQuadrature.upper (n : ℕ) (u : ℝ) : ℝ

Equations

• G12SharpQuadrature.upper n u = (561990 / 1000000 + (564383 / 1000000 - 561990 / 1000000) * G12SharpQuadrature.step n u) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight u

theorem G12SharpQuadrature.step_bounds (n : ℕ) (u : ℝ) : 0 ≤ step n u ∧ step n u ≤ 1

theorem G12SharpQuadrature.step_high (n : ℕ) {u : ℝ} (hu : 1 / 10 ≤ u) : step n u = 1

theorem G12SharpQuadrature.upper_bounds (n : ℕ) (u : ℝ) : 0 ≤ upper n u ∧ upper n u ≤ 8

theorem G12SharpQuadrature.sharp_le_upper (n : ℕ) (u : ℝ) : G12SharpWeight.weight u ≤ upper n u

theorem G12SharpQuadrature.continuousOn_upper (n : ℕ) : ContinuousOn (upper n) (Set.Icc (4 / 53) (4 / 33))

theorem G12SharpQuadrature.kernel_mono (h g : ℝ → ℝ) (hh : ∀ u ∈ Set.Icc (4 / 53) (4 / 33), h u ≤ g u) {N : ℕ} (hN : 4 ≤ N) : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel h N ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel g N

All original labels, including repeated primes and endpoints, are retained.