Liu's reciprocal-log main integral

This file defines the exact source integral and the uniform prime-sum transfer predicate behind Liu's printed 0.49254 estimate. The downstream logarithmic grid development proves the transfer predicate.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceInnerIntegrand (α β : ℝ) : ℝ

The integrand in the inner integral printed in Liu's lm-mt.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceInnerIntegrand α β = 1 / (β * (1 - α - β))

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceInnerIntegral (α : ℝ) : ℝ

The inner integral in Liu's lm-mt.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceInnerIntegral α = ∫ (β : ℝ) in 1 / 3..(1 - α) / 2, MathlibNt.SieveTheory.LiuWeight.liuSourceInnerIntegrand α β

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceMainIntegral : ℝ

The source double integral in Liu's lm-mt.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceMainIntegral = ∫ (α : ℝ) in 1 / 10..1 / 3, 1 / α * MathlibNt.SieveTheory.LiuWeight.liuSourceInnerIntegral α

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceReducedIntegrand (α : ℝ) : ℝ

The one-dimensional integrand obtained after evaluating Liu's inner integral.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceReducedIntegrand α = Real.log (2 - 3 * α) / (α * (1 - α))

theorem MathlibNt.SieveTheory.LiuWeight.liuSource_inner_domain_pos {α β : ℝ} (hα : α ∈ Set.Icc (1 / 10) (1 / 3)) (hβ : β ∈ Set.Icc (1 / 3) ((1 - α) / 2)) : 0 < β ∧ 0 < 1 - α - β

theorem MathlibNt.SieveTheory.LiuWeight.liuSource_inner_intervalIntegrable {α : ℝ} (hα : α ∈ Set.Icc (1 / 10) (1 / 3)) : IntervalIntegrable (liuSourceInnerIntegrand α) MeasureTheory.volume (1 / 3) ((1 - α) / 2)

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceInnerIntegral_eq {α : ℝ} (hα : α ∈ Set.Icc (1 / 10) (1 / 3)) : liuSourceInnerIntegral α = Real.log (2 - 3 * α) / (1 - α)

Exact evaluation of the inner integral in Liu's lm-mt.

theorem MathlibNt.SieveTheory.LiuWeight.liuSource_reduced_intervalIntegrable : IntervalIntegrable liuSourceReducedIntegrand MeasureTheory.volume (1 / 10) (1 / 3)

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceMainIntegral_eq_reduced : liuSourceMainIntegral = ∫ (α : ℝ) in 1 / 10..1 / 3, liuSourceReducedIntegrand α

Liu's double integral is exactly the reduced one-dimensional integral.

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceMainIntegral_lt : liuSourceMainIntegral < 0.49254

Liu's source main integral is strictly below the printed constant.

def MathlibNt.SieveTheory.LiuWeight.LiuSourceMainIntegralConstantBound : Prop

The purely symbolic constant inequality used in Liu's transfer argument.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuSourceMainIntegralConstantBound = (MathlibNt.SieveTheory.LiuWeight.liuSourceMainIntegral < 0.49254)

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceMainIntegralConstantBound : LiuSourceMainIntegralConstantBound

The source main integral satisfies its named constant-bound predicate.

def MathlibNt.SieveTheory.LiuWeight.LiuSourcePrimeSumToIntegralTransfer : Prop

A source-faithful, uniform eventual transfer from Liu's finite prime-pair sum to the source integral. Its quantifier order fixes the grid before choosing the finite-N threshold.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuSourcePrimeSumToIntegralTransfer = ∀ (η : ℝ), 0 < η → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Real.log ↑N * MathlibNt.SieveTheory.LiuWeight.liuSourceReciprocalLogSum N ≤ MathlibNt.SieveTheory.LiuWeight.liuSourceMainIntegral + η

def MathlibNt.SieveTheory.LiuWeight.LiuSourceMainIntegralMargin (δ : ℝ) : Prop

An explicit positive margin below Liu's printed decimal.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuSourceMainIntegralMargin δ = (0 < δ ∧ MathlibNt.SieveTheory.LiuWeight.liuSourceMainIntegral ≤ 0.49254 - δ)

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuSourceReciprocalLogBound_of_transfer_of_margin (htransfer : LiuSourcePrimeSumToIntegralTransfer) {δ : ℝ} (hmargin : LiuSourceMainIntegralMargin δ) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → LiuSourceReciprocalLogBound N

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuSourceReciprocalLogBound_of_transfer_of_constantBound (htransfer : LiuSourcePrimeSumToIntegralTransfer) (hconstant : LiuSourceMainIntegralConstantBound) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → LiuSourceReciprocalLogBound N