@[instance_reducible]

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

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_corner_pos {n : ℕ} (hn : 0 < n) {δ : ℝ} (hδ : δ ≤ 1 / 4) (q : Fin n × Fin n) : 0 < fouvryG9RelaxedIntegralCorner n δ q

Corner denominators stay positive uniformly, including coarse grids.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_term_le_corner {n N : ℕ} (hn : 0 < n) {ρ δ : ℝ} (hN : 2 ≤ N) (hρ : 1 < ρ) (hδ : δ ≤ 1 / 4) (q : Fin n × Fin n) (rs : ℕ × ℕ) (hrect : LiuWeight.LiuPairInLogRectangle N (goldbachB9AlphaGridPoint n ↑q.1) (goldbachB9AlphaGridPoint n (↑q.1 + 1)) (goldbachB9BetaGridPoint n ↑q.2) (goldbachB9BetaGridPoint n (↑q.2 + 1)) rs) (hr : Nat.Prime rs.1) (hs : Nat.Prime rs.2) : 1 / (↑rs.1 * ↑rs.2 * (1 + 3 * Real.log ρ / Real.log ↑N - LiuWeight.primeLogExponent N rs.1 - LiuWeight.primeLogExponent N rs.2) * (5 / 9 * (1 - LiuWeight.primeLogExponent N rs.1) - δ)) ≤ fouvryG9RelaxedIntegralCorner n δ q * (1 / (↑rs.1 * ↑rs.2))

The true moving kernel is bounded by a fixed upper-corner weight.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_rectangle_subset {N : ℕ} (hN : 2 ≤ N) (ρ a₀ a₁ b₀ b₁ : ℝ) : Finset.filter (LiuWeight.LiuPairInLogRectangle N a₀ a₁ b₀ b₁) (fouvryG9RelaxedPairs N ρ) ⊆ LiuWeight.primeLogRectanglePairs N a₀ a₁ b₀ b₁

Source membership is used only for primality when enlarging to a rectangle.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_kernel_le_grid (n N : ℕ) (hn : 0 < n) (hN : 2 ≤ N) {ρ h δ : ℝ} (hρ : 1 < ρ) (hδ : δ ≤ 1 / 4) (hh : h ≤ 1 / 20) (hw : 1 + 3 * Real.log ρ / Real.log ↑N ≤ 1 + h) : fouvryG9RelaxedPairKernel N ρ δ ≤ fouvryG9RelaxedIntegralGrid n N h δ

Named finite bridge: the actual relaxed kernel is bounded by a fixed finite prime-reciprocal grid. No asymptotic premise or integral bound is assumed.