@[instance_reducible]

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

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10BadActualAtoms_le_four_hundred_badCount {N : ℕ} {ε β γ : ℝ} (hε : 0 < ε) (hβ : 1 / 21 < β) : ↑(goldbachG10BadActualAtoms N ε (↑N ^ β) (↑N ^ γ)).card ≤ 400 * goldbachBadCount (goldbachDifferenceCarrier N ε) N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10RSquareActualAtoms_le_twenty_mul_goldbachQA {N : ℕ} {ε β γ : ℝ} (hε : 0 < ε) (hβ0 : 1 / 21 < β) : ↑(goldbachG10RSquareActualAtoms N ε (↑N ^ β) (↑N ^ γ)).card ≤ 20 * goldbachQA (goldbachDifferenceCarrier N ε) N (↑N ^ β)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10SSquareActualAtoms_le_twenty_mul_goldbachQA {N : ℕ} {ε β γ : ℝ} (hε : 0 < ε) (hβ0 : 1 / 21 < β) : ↑(goldbachG10SSquareActualAtoms N ε (↑N ^ β) (↑N ^ γ)).card ≤ 20 * goldbachQA (goldbachDifferenceCarrier N ε) N (↑N ^ β)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Corrected_actual_le_pi10_with_errors {N : ℕ} {ε β γ : ℝ} (hε : 0 < ε) (hβ : 1 / 18 < β) (hβγ : β < (1 - 3 * β) / 3) (hγ : (1 - 3 * β) / 3 < γ) (hcut : 1 < ε * ↑N ^ (1 / 6)) : goldbachG10Corrected (goldbachDifferenceCarrier N ε) N (↑N ^ β) (↑N ^ γ) ≤ goldbachPi10 N ε (↑N ^ β) (↑N ^ γ) + 400 * goldbachBadCount (goldbachDifferenceCarrier N ε) N + 40 * goldbachQA (goldbachDifferenceCarrier N ε) N (↑N ^ β)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachG10SwitchFinite_cutoff (ε : ℝ) (hε : 0 < ε) : ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → 1 < ε * ↑N ^ (1 / 6)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Corrected_actual_eventually_le_pi10_with_errors (ε : ℝ) (hε : 0 < ε) : ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → ∀ (β γ : ℝ), 1 / 18 < β → β < (1 - 3 * β) / 3 → (1 - 3 * β) / 3 < γ → γ < 1 / 3 → goldbachG10Corrected (goldbachDifferenceCarrier N ε) N (↑N ^ β) (↑N ^ γ) ≤ goldbachPi10 N ε (↑N ^ β) (↑N ^ γ) + 400 * goldbachBadCount (goldbachDifferenceCarrier N ε) N + 40 * goldbachQA (goldbachDifferenceCarrier N ε) N (↑N ^ β)