@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachB10PanTwoEndpoints (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachB10PanTwoEndpoints P = Classical.propDecidable P

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanPrefixRemainder_twoEndpoints_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (K : ℕ), ∀ {N Y D A₁ A₂ : ℕ} {ε b c : ℝ}, Y = ⌊ε * ↑N⌋₊ → K ≤ N → K ≤ Y → 0 < ε → ε < 1 → (∀ ⦃m : ℕ⦄, m ∈ goldbachC10ProductSupport N b c → m ∈ Finset.Ioc A₁ A₂) → ↑A₂ ≤ ↑N ^ (2 / 3) → ↑A₂ ≤ ↑Y ^ (2 / 3) → Real.log ↑N ^ (2 * B) ≤ ↑A₁ → Real.log ↑Y ^ (2 * B) ≤ ↑A₁ → D ≤ LiuWeight.panModulusCutoff N B → D ≤ LiuWeight.panModulusCutoff Y B → ∑ d ∈ Finset.Icc 1 D with d.Coprime N, |goldbachB10PanPrefixRemainder N d A₁ A₂ ε b c| ≤ C * (↑N / Real.log ↑N ^ U + ↑Y / Real.log ↑Y ^ U)

Two-endpoint aggregate bound for the actual finite B10 Pan remainder, consuming the existing bounded-coefficient Pan aggregate theorem at N and at the lower endpoint Y = ⌊εN⌋. The geometric support hypotheses remain explicit.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanPrefixRemainder_floor_twoEndpoints_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (K : ℕ), ∀ {N D A₁ A₂ : ℕ} {ε b c : ℝ}, K ≤ N → K ≤ ⌊ε * ↑N⌋₊ → 0 < ε → ε < 1 → (∀ ⦃m : ℕ⦄, m ∈ goldbachC10ProductSupport N b c → m ∈ Finset.Ioc A₁ A₂) → ↑A₂ ≤ ↑N ^ (2 / 3) → ↑A₂ ≤ ↑⌊ε * ↑N⌋₊ ^ (2 / 3) → Real.log ↑N ^ (2 * B) ≤ ↑A₁ → Real.log ↑⌊ε * ↑N⌋₊ ^ (2 * B) ≤ ↑A₁ → D ≤ LiuWeight.panModulusCutoff N B → D ≤ LiuWeight.panModulusCutoff ⌊ε * ↑N⌋₊ B → ∑ d ∈ Finset.Icc 1 D with d.Coprime N, |goldbachB10PanPrefixRemainder N d A₁ A₂ ε b c| ≤ C * (↑N / Real.log ↑N ^ U + ↑⌊ε * ↑N⌋₊ / Real.log ↑⌊ε * ↑N⌋₊ ^ U)

Direct floor-endpoint form of the two-endpoint aggregate bound.