MathlibNt.SieveTheory.LiLiuGoldbachWeightG11GoodConsumed

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11GoodRemainder (N : ℕ) (ε : ℝ) :

ℤ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11GoodRemainder N ε = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11RoughRemainder N ε + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughTotal N ε - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33))

Instances For

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11GoodRemainder · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughTotal_le_goodSwitched_normalized (δ : ℝ) (hδ : 0 < δ) :

∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ), 0 ≤ ε → ↑(goldbachG11RoughTotal N ε) ≤ ↑(goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) + δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughTotal_le_goodSwitched_normalized · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_le_goodSwitched_normalized (δ : ℝ) (hδ : 0 < δ) :

∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ), 0 ≤ ε → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ ↑(goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) + δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_le_goodSwitched_normalized · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_g11GoodSwitched_consumed_eventually (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) :

∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (Z : ℝ), 1 ≤ Z → Z ≤ √↑N → ↑(goldbachWeightG11GoodRemainder N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Z) + (goldbachWeightHighFirstCoefficient ε - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

The coprime switched G11 count remains literal; only finite exceptional losses are paid.

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_g11GoodSwitched_consumed_eventually · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_g11GoodSwitched_consumed_small_epsilon (δ : ℝ) (hδ : 0 < δ) :

∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (Z : ℝ), 1 ≤ Z → Z ≤ √↑N → ↑(goldbachWeightG11GoodRemainder N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Z) + (goldbachWeightHighFirstCoefficient 0 - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_g11GoodSwitched_consumed_small_epsilon · compiled type and proof/definition references.