@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidablePropB8LogKernel (p : Prop) : Decidable p

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidablePropB8LogKernel p = Classical.propDecidable p

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8Gamma : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8Gamma = 3 / 11

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8Pair_logGeometry {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachS4Pairs N (↑N ^ (3 / 11))) : goldbachB8Gamma ≤ LiuWeight.primeLogExponent N rs.1 ∧ LiuWeight.primeLogExponent N rs.1 ≤ 1 / 3 ∧ LiuWeight.primeLogExponent N rs.1 ≤ LiuWeight.primeLogExponent N rs.2 ∧ LiuWeight.primeLogExponent N rs.1 + 2 * LiuWeight.primeLogExponent N rs.2 ≤ 1

The closed logarithmic geometry of the actual S4 carrier, including the diagonal.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PrimeLogExponent_second_le_upper {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachS4Pairs N (↑N ^ (3 / 11))) : LiuWeight.primeLogExponent N rs.2 ≤ 4 / 11

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8OneSubPrimeLogExponent_pos {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachS4Pairs N (↑N ^ (3 / 11))) : 0 < 1 - LiuWeight.primeLogExponent N rs.1 - LiuWeight.primeLogExponent N rs.2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogProd_eq {N : ℕ} {rs : ℕ × ℕ} (hrs : rs ∈ goldbachS4Pairs N (↑N ^ (3 / 11))) : Real.log ↑(goldbachC8Prod rs) = Real.log ↑rs.1 + Real.log ↑rs.2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairLogKernelTerm_eq {N : ℕ} {rs : ℕ × ℕ} (hrs : rs ∈ goldbachS4Pairs N (↑N ^ (3 / 11))) : 1 / (↑(goldbachC8Prod rs) * (1 - Real.log ↑(goldbachC8Prod rs) / Real.log ↑N)) = LiuWeight.liuPairLogKernel N rs

This is an identity on the actual carrier, not a replacement by all prime pairs.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairLogKernel_eq_logCoordinateSum (N : ℕ) : goldbachB8PairLogKernel N = ∑ rs ∈ goldbachS4Pairs N (↑N ^ (3 / 11)), LiuWeight.liuPairLogKernel N rs

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairLogKernelTerm_nonneg {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachS4Pairs N (↑N ^ (3 / 11))) : 0 ≤ LiuWeight.liuPairLogKernel N rs

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairsInLogRectangle (N : ℕ) (a₀ a₁ b₀ b₁ : ℝ) : Finset (ℕ × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairsInLogRectangle N a₀ a₁ b₀ b₁ = Finset.filter (MathlibNt.SieveTheory.LiuWeight.LiuPairInLogRectangle N a₀ a₁ b₀ b₁) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs N (↑N ^ (3 / 11)))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairLogKernelRectangleContribution (N : ℕ) (a₀ a₁ b₀ b₁ : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairLogKernelRectangleContribution N a₀ a₁ b₀ b₁ = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairsInLogRectangle N a₀ a₁ b₀ b₁, MathlibNt.SieveTheory.LiuWeight.liuPairLogKernel N rs

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairsInLogRectangle_subset_primeLogRectanglePairs {N : ℕ} (hN : 2 ≤ N) (a₀ a₁ b₀ b₁ : ℝ) : goldbachB8PairsInLogRectangle N a₀ a₁ b₀ b₁ ⊆ LiuWeight.primeLogRectanglePairs N a₀ a₁ b₀ b₁

Only a subset inclusion: the target rectangle drops coprimality and source geometry.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairLogKernelTerm_le_rectangleCorner {N : ℕ} {rs : ℕ × ℕ} {a₀ a₁ b₀ b₁ : ℝ} (hrect : LiuWeight.LiuPairInLogRectangle N a₀ a₁ b₀ b₁ rs) (hupper : a₁ + b₁ < 1) : LiuWeight.liuPairLogKernel N rs ≤ 1 / (1 - a₁ - b₁) * (1 / (↑rs.1 * ↑rs.2))

The coordinate kernel is generic; no Liu or C10 carrier theorem is used here.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairLogKernelRectangleContribution_le (N : ℕ) (hN : 2 ≤ N) (a₀ a₁ b₀ b₁ : ℝ) (hupper : a₁ + b₁ < 1) : goldbachB8PairLogKernelRectangleContribution N a₀ a₁ b₀ b₁ ≤ 1 / (1 - a₁ - b₁) * PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N a₀ a₁ b₀ b₁