theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_denominators {u v w δ : ℝ} (hu : u ≤ 1 / 10) (hv : u + 2 * v ≤ 1 + 1 / 20) (hw : 1 ≤ w) (hδ : δ ≤ 1 / 4) : 17 / 40 ≤ 1 - u - v ∧ 17 / 40 ≤ w - u - v ∧ 1 / 4 ≤ 5 / 9 * (1 - u) - δ

Uniformly positive denominators on a slightly enlarged low strip.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_static_majorant {r s u v w δ : ℝ} (hr : 0 < r) (hs : 0 < s) (hu : u ≤ 1 / 10) (hv : u + 2 * v ≤ 1 + 1 / 20) (hw : 1 ≤ w) (hδ : δ ≤ 1 / 4) : 1 / (r * s * (w - u - v) * (5 / 9 * (1 - u) - δ)) ≤ 1 / (r * s * (1 - u - v) * (5 / 9 * (1 - u) - δ))

The moving first denominator is safely replaced by the smaller static one.

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

The literal production weighted low integral (the production API is a theorem, not a constant named goldbachB9WeightedSubintervalIntegral).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralLow = ∫ (u : ℝ) in 4 / 53..1 / 10, ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v) * (1 - u))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralLow_eq_single : fouvryG9RelaxedIntegralLow = ∫ (u : ℝ) in 4 / 53..1 / 10, Real.log (2 - 3 * u) / (u * (1 - u) ^ 2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_geometry {N : ℕ} {ρ : ℝ} (hN : 2 ≤ N) (hρ : 1 < ρ) {rs : ℕ × ℕ} (hrs : rs ∈ fouvryG9RelaxedPairs N ρ) : 4 / 53 ≤ LiuWeight.primeLogExponent N rs.1 ∧ LiuWeight.primeLogExponent N rs.1 < 1 / 10 ∧ 1 / 3 ≤ LiuWeight.primeLogExponent N rs.2 ∧ LiuWeight.primeLogExponent N rs.1 + 2 * LiuWeight.primeLogExponent N rs.2 ≤ 1 + 3 * Real.log ρ / Real.log ↑N

Exact logarithmic geometry of the actual relaxed carrier.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralCells (n : ℕ) (h : ℝ) : Finset (Fin n × Fin n)

The grid is fixed before N; h is a fixed boundary-strip width.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralCells n h = {q : Fin n × Fin n | 4 / 53 ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n (↑q.1 + 1) ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n ↑q.1 < 1 / 10 ∧ 1 / 3 ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n (↑q.2 + 1) ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n ↑q.1 + 2 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n ↑q.2 < 1 + h}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralCorner (n : ℕ) (δ : ℝ) (q : Fin n × Fin n) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralCorner n δ q = 1 / ((1 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n (↑q.1 + 1) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n (↑q.2 + 1)) * (5 / 9 * (1 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n (↑q.1 + 1)) - δ))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralGrid (n N : ℕ) (h δ : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralGrid n N h δ = ∑ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralCells n h, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralCorner n δ q * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n ↑q.1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n (↑q.1 + 1)) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n ↑q.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n (↑q.2 + 1))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralUpperSum (n : ℕ) (h δ : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralUpperSum n h δ = ∑ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralCells n h, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralCorner n δ q * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n ↑q.1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n (↑q.1 + 1)) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n ↑q.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n (↑q.2 + 1))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_fixed_grid_tendsto (n : ℕ) (hn : 0 < n) (h δ : ℝ) : Filter.Tendsto (fun (N : ℕ) => fouvryG9RelaxedIntegralGrid n N h δ) Filter.atTop (nhds (fouvryG9RelaxedIntegralUpperSum n h δ))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_cover (n N : ℕ) (hn : 0 < n) (hN : 2 ≤ N) {ρ h : ℝ} (hρ : 1 < ρ) (hh : h ≤ 1 / 20) (hw : 1 + 3 * Real.log ρ / Real.log ↑N ≤ 1 + h) {rs : ℕ × ℕ} (hrs : rs ∈ fouvryG9RelaxedPairs N ρ) : ∃ q ∈ fouvryG9RelaxedIntegralCells n h, LiuWeight.LiuPairInLogRectangle N (goldbachB9AlphaGridPoint n ↑q.1) (goldbachB9AlphaGridPoint n (↑q.1 + 1)) (goldbachB9BetaGridPoint n ↑q.2) (goldbachB9BetaGridPoint n (↑q.2 + 1)) rs

Every closed lower boundary is captured inside a left-open grid cell.