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

The original closed cross kernel. Repeated primes are retained.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel h N = ∑ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), 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.goldbachG12PrimeIntegral (h : ℝ → ℝ) : ℝ

The fourth variable has the independent cross interval, not the G11 interval.

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_prime_ne_cross_cutoff (N p : ℕ) (hp : Nat.Prime p) : ↑p ≠ ↑N ^ (4 / 33)

The cross junction cannot be a prime, by its prime valuation.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_prime_cross_cutoff_iff (N p : ℕ) (hp : Nat.Prime p) : ↑N ^ (4 / 33) ≤ ↑p ↔ ↑N ^ (4 / 33) < ↑p

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel_logGeometry {N : ℕ} (hN : 4 ≤ N) {v : GoldbachG11Label} (hv : v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) : Real.log ↑v.snd.snd.fst / Real.log ↑N ∈ Set.Icc (4 / 53) (4 / 33) ∧ 0 < Real.log ↑v.snd.snd.snd

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

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