noncomputable def G12SharpWeight.factor (u : ℝ) : ℝ

The original low/high Buchstab bounds, with the junction assigned high.

Equations

• G12SharpWeight.factor u = if u < 1 / 10 then 561990 / 1000000 else 564383 / 1000000

noncomputable def G12SharpWeight.weight (u : ℝ) : ℝ

Equations

• G12SharpWeight.weight u = G12SharpWeight.factor u * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight u

theorem G12SharpWeight.factor_nonneg (u : ℝ) : 0 ≤ factor u

theorem G12SharpWeight.factor_le_one (u : ℝ) : factor u ≤ 1

theorem G12SharpWeight.weight_nonneg (u : ℝ) : 0 ≤ weight u

theorem G12SharpWeight.weight_le_eight (u : ℝ) : weight u ≤ 8