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

The fixed lower exponent β = 4/33 from Liu's printed I10.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Beta = 4 / 33

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

The fixed upper/lower exponent γ = 3/11 from Liu's printed I10.

Equations

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

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairInLogRectangle (N : ℕ) (a₀ a₁ b₀ b₁ : ℝ) (rs : ℕ × ℕ) : Prop

The exact C10 kernel rectangle predicate in logarithmic coordinates.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairInLogRectangle N a₀ a₁ b₀ b₁ rs = (a₀ < MathlibNt.SieveTheory.LiuWeight.primeLogExponent N rs.1 ∧ MathlibNt.SieveTheory.LiuWeight.primeLogExponent N rs.1 ≤ a₁ ∧ b₀ < MathlibNt.SieveTheory.LiuWeight.primeLogExponent N rs.2 ∧ MathlibNt.SieveTheory.LiuWeight.primeLogExponent N rs.2 ≤ b₁)

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

The C10 pairs whose logarithmic coordinates lie in one fixed rectangle.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairsInLogRectangle N a₀ a₁ b₀ b₁ = Finset.filter (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairInLogRectangle N a₀ a₁ b₀ b₁) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N (↑N ^ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Beta) (↑N ^ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Gamma))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairLogKernel (N : ℕ) (rs : ℕ × ℕ) : ℝ

The exact logarithmic kernel on the actual ordered C10 prime pairs.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairLogKernel N rs = 1 / (↑rs.1 * ↑rs.2 * (1 - MathlibNt.SieveTheory.LiuWeight.primeLogExponent N rs.1 - MathlibNt.SieveTheory.LiuWeight.primeLogExponent N rs.2))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairLogKernelSum (N : ℕ) : ℝ

The actual finite C10 logarithmic-kernel sum corresponding to I10.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairLogKernelSum N = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N (↑N ^ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Beta) (↑N ^ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Gamma), MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairLogKernel N rs

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

The contribution from the actual C10 pairs lying in one fixed exponent rectangle.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairLogKernelRectangleContribution N a₀ a₁ b₀ b₁ = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairsInLogRectangle N a₀ a₁ b₀ b₁, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairLogKernel N rs

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeLogExponent_add_two_mul_le_one {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma)) : LiuWeight.primeLogExponent N rs.1 + 2 * LiuWeight.primeLogExponent N rs.2 ≤ 1

The actual C10 product condition becomes α + 2β ≤ 1 in logarithmic coordinates.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeLogExponent_ge_beta {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma)) : goldbachB10Beta ≤ LiuWeight.primeLogExponent N rs.1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeLogExponent_le_gamma {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma)) : LiuWeight.primeLogExponent N rs.1 ≤ goldbachB10Gamma

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeLogExponent_second_pos {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma)) : 0 < LiuWeight.primeLogExponent N rs.2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeLogExponent_second_le_upper {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma)) : LiuWeight.primeLogExponent N rs.2 ≤ 29 / 66

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10OneSubPrimeLogExponent_pos {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma)) : 0 < 1 - LiuWeight.primeLogExponent N rs.1 - LiuWeight.primeLogExponent N rs.2

The remaining kernel denominator is strictly positive on the actual C10 carrier.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairLogKernelSum_le_sum_rectangleMajorants_of_cover {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (a₀ a₁ b₀ b₁ : ι → ℝ) (N : ℕ) (hN : 2 ≤ N) (_ha₀ : ∀ i ∈ s, 0 < a₀ i) (_ha : ∀ i ∈ s, a₀ i < a₁ i) (_hb₀ : ∀ i ∈ s, 0 < b₀ i) (_hb : ∀ i ∈ s, b₀ i < b₁ i) (hupper : ∀ i ∈ s, a₁ i + b₁ i < 1) (hcover : ∀ rs ∈ goldbachC10Pairs N (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma), ∃ i ∈ s, goldbachB10PairInLogRectangle N (a₀ i) (a₁ i) (b₀ i) (b₁ i) rs) : goldbachB10PairLogKernelSum N ≤ ∑ i ∈ s, 1 / (1 - a₁ i - b₁ i) * PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N (a₀ i) (a₁ i) (b₀ i) (b₁ i)

A finite family of fixed positive rectangles may overlap: if it covers every actual C10 pair and stays below u + v = 1, then the full C10 logarithmic-kernel sum is bounded by the sum of the rectangle majorants.