noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeKernel (h : ℝ → ℝ) (N : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeKernel h N = ∑ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), h (Real.log ↑v.snd.snd.fst / Real.log ↑N) * Real.log ↑N / (↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v) * Real.log ↑v.snd.snd.snd)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral (h : ℝ → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral h = ∫ (r : ℝ) in 4 / 53..4 / 33, ∫ (q : ℝ) in r..4 / 33, ∫ (s : ℝ) in q..4 / 33, ∫ (t : ℝ) in s..4 / 33, h r / (r * q ^ 2 * s * t)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeKernel_const (c : ℝ) (N : ℕ) : goldbachG11PrimeKernel (fun (x : ℝ) => c) N = c * goldbachG11PrimeKernel (fun (x : ℝ) => 1) N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeKernel_logGeometry {N : ℕ} (hN : 4 ≤ N) {v : GoldbachG11Label} (hv : v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) : Real.log ↑v.snd.snd.fst / Real.log ↑N ∈ Set.Icc (4 / 53) (4 / 33) ∧ 0 < Real.log ↑v.snd.snd.snd ∧ Real.log (↑N / ↑(goldbachG11LabelProd v)) / Real.log ↑v.snd.snd.snd ∈ Set.Icc (17 / 4) (37 / 4)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeKernel_nonneg (h : ℝ → ℝ) (hh : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), 0 ≤ h x) {N : ℕ} (hN : 4 ≤ N) : 0 ≤ goldbachG11PrimeKernel h N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BuchstabUpperMass_le_primeKernel {N : ℕ} (hN : 4 ≤ N) (η W : ℝ) (_hη : 0 ≤ η) (hW : ∀ u ∈ Set.Icc (17 / 4) (37 / 4), LiLiuPrereqBuchstab.buchstab u ≤ W) : Real.log ↑N / ↑N * goldbachG11BuchstabUpperMass N η ≤ (W + η) * goldbachG11PrimeKernel (fun (x : ℝ) => 1) N

Only the raw pointwise Buchstab bound is supplied by the caller.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BuchstabUpperMass_le_primeKernel_one {N : ℕ} (hN : 4 ≤ N) (η : ℝ) (hη : 0 ≤ η) : Real.log ↑N / ↑N * goldbachG11BuchstabUpperMass N η ≤ (1 + η) * goldbachG11PrimeKernel (fun (x : ℝ) => 1) N

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight (r : ℝ) : ℝ

The minimum encodes the matching two branches without a discontinuity.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight r = 36 / (5 * (1 - min r (1 / 10)))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight_eq_low {r : ℝ} (hr : r ≤ 1 / 10) : goldbachG11AuthorWeight r = 36 / (5 * (1 - r))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight_eq_high {r : ℝ} (hr : 1 / 10 ≤ r) : goldbachG11AuthorWeight r = 8

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight_at_join : goldbachG11AuthorWeight (1 / 10) = 8 ∧ 36 / (5 * (1 - 1 / 10)) = 8

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight_nonneg (r : ℝ) : 0 ≤ goldbachG11AuthorWeight r

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuous_goldbachG11AuthorWeight : Continuous goldbachG11AuthorWeight

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuousOn_goldbachG11AuthorWeight : ContinuousOn goldbachG11AuthorWeight (Set.Icc (4 / 53) (4 / 33))