@[instance_reducible]

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

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9Pair_logGeometry {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) : 4 / 53 ≤ LiuWeight.primeLogExponent N rs.1 ∧ LiuWeight.primeLogExponent N rs.1 ≤ 1 / 3 ∧ 1 / 3 ≤ LiuWeight.primeLogExponent N rs.2 ∧ LiuWeight.primeLogExponent N rs.1 + 2 * LiuWeight.primeLogExponent N rs.2 ≤ 1

Closed C10 geometry, with no deletion of endpoints or repeated factors.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PrimeLogExponent_second_le_upper {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) : LiuWeight.primeLogExponent N rs.2 ≤ 1 / 2

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogProd_eq {N : ℕ} {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) : Real.log ↑(goldbachC10Prod rs) = Real.log ↑rs.1 + Real.log ↑rs.2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PairLogKernelTerm_eq {N : ℕ} {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) : 1 / (↑(goldbachC10Prod rs) * (1 - Real.log ↑(goldbachC10Prod rs) / Real.log ↑N)) = LiuWeight.liuPairLogKernel N rs

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PairLogKernel_eq_logCoordinateSum (N : ℕ) : goldbachB9PairLogKernel N = ∑ rs ∈ goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)), LiuWeight.liuPairLogKernel N rs

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PairLogKernelTerm_nonneg {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) : 0 ≤ LiuWeight.liuPairLogKernel N rs

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PairLogKernel_nonneg {N : ℕ} (hN : 2 ≤ N) : 0 ≤ goldbachB9PairLogKernel N

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PairsInLogRectangle N a₀ a₁ b₀ b₁ = Finset.filter (MathlibNt.SieveTheory.LiuWeight.LiuPairInLogRectangle N a₀ a₁ b₀ b₁) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)))

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

Equations

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

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

Coprimality and source geometry are dropped only in this upper-bound inclusion.

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