noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstSupport (N : ℕ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstSupport N = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductSupport N (↑N ^ (1 / 10)) (↑N ^ (1 / 3))

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

The genuine high zero-prefix mass: Li0(N/m), without subtracting Li0(0).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachX9High N = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusLiWeight N m

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachK9High N = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)), 1 / (↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs) * (1 - Real.log ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod rs) / Real.log ↑N))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstSupport_subset (N : ℕ) (hN : 2 ≤ N) : goldbachB9HighFirstSupport N ⊆ goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachX9High_eq_pair_sum (N : ℕ) : goldbachX9High N = ∑ rs ∈ goldbachC10Pairs N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)), LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑(goldbachC10Prod rs))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachK9High_eq_support_sum (N : ℕ) : goldbachK9High N = ∑ m ∈ goldbachB9HighFirstSupport N, 1 / (↑m * (1 - Real.log ↑m / Real.log ↑N))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstLiWeight_bounds_eventually : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ m ∈ goldbachB9HighFirstSupport N, 2 ≤ ↑N / ↑m ∧ 0 ≤ goldbachB9PlusLiWeight N m ∧ |goldbachB9PlusLiWeight N m| ≤ 2 * ↑N / ↑m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachX9High_nonneg_eventually : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → 0 ≤ goldbachX9High N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirst_gate_le_full (N : ℕ) (hN : 2 ≤ N) (hw : ∀ m ∈ goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)), 0 ≤ goldbachB9PlusLiWeight N m) (d : ℕ) : gateLoss N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) (goldbachB9PlusLiWeight N) d ≤ gateLoss N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (goldbachB9PlusLiWeight N) d

Positivity is established before comparing the two absolute gate losses.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirst_gate_log_saving (U : ℝ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ Q ≤ N, ∑ d ∈ Finset.Icc 1 Q, gateLoss N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) (goldbachB9PlusLiWeight N) d ≤ ↑N / Real.log ↑N ^ U

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachK9High_nonneg (N : ℕ) (hN : 2 ≤ N) : 0 ≤ goldbachK9High N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirst_proxy_eq (N : ℕ) (hN : 2 ≤ N) : ∑ m ∈ goldbachB9HighFirstSupport N, ↑N / ↑m / Real.log (↑N / ↑m) = ↑N / Real.log ↑N * goldbachK9High N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachX9High_le_kernel_eventually (τ : ℝ) (hτ : 0 < τ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachX9High N ≤ (1 + τ) * (↑N / Real.log ↑N) * goldbachK9High N