theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel_eq_logCoordinateSum (h : ℝ → ℝ) (N : ℕ) : goldbachG12PrimeKernel h N = ∑ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), h (Real.log ↑v.snd.snd.fst / Real.log ↑N) / (Real.log ↑v.snd.snd.snd / Real.log ↑N) * (1 / ↑(goldbachG11LabelProd v))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeBoxContribution (h : ℝ → ℝ) (N : ℕ) (lo hi : Fin 4 → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeBoxContribution h N lo hi = ∑ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)) with v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeBox N lo hi, 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)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeBoxContribution_le (h : ℝ → ℝ) {N : ℕ} (hN : 4 ≤ N) (lo hi : Fin 4 → ℝ) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ r ∈ Set.Ioc (lo 0) (hi 0), ∀ q ∈ Set.Ioc (lo 1) (hi 1), h r / q ≤ C) : goldbachG12PrimeBoxContribution h N lo hi ≤ C * goldbachG11PrimeBoxMass N lo hi

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel_le_boxCover {ι : Type u_1} (S : Finset ι) (h : ℝ → ℝ) (hh : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), 0 ≤ h x) {N : ℕ} (hN : 4 ≤ N) (lo hi : ι → Fin 4 → ℝ) (C : ι → ℝ) (hC : ∀ j ∈ S, 0 ≤ C j) (hbound : ∀ j ∈ S, ∀ r ∈ Set.Ioc (lo j 0) (hi j 0), ∀ q ∈ Set.Ioc (lo j 1) (hi j 1), h r / q ≤ C j) (hcover : ∀ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), ∃ j ∈ S, v ∈ goldbachG11PrimeBox N (lo j) (hi j)) : goldbachG12PrimeKernel h N ≤ ∑ j ∈ S, C j * goldbachG11PrimeBoxMass N (lo j) (hi j)

Finite covers may overlap. This is not an assumption about a prime-to-integral limit.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel_le_fixedCover_eventually {ι : Type u_1} (S : Finset ι) (h : ℝ → ℝ) (hh : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), 0 ≤ h x) (lo hi : ι → Fin 4 → ℝ) (C : ι → ℝ) (hlo : ∀ j ∈ S, ∀ (i : Fin 4), 0 < lo j i) (hhi : ∀ j ∈ S, ∀ (i : Fin 4), lo j i < hi j i) (hC : ∀ j ∈ S, 0 ≤ C j) (hbound : ∀ j ∈ S, ∀ r ∈ Set.Ioc (lo j 0) (hi j 0), ∀ q ∈ Set.Ioc (lo j 1) (hi j 1), h r / q ≤ C j) (hcover : ∀ (N : ℕ), 4 ≤ N → ∀ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), ∃ j ∈ S, v ∈ goldbachG11PrimeBox N (lo j) (hi j)) (ν : ℝ) (hν : 0 < ν) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachG12PrimeKernel h N ≤ ∑ j ∈ S, C j * goldbachG11LogBoxMass (lo j) (hi j) + ν