Documentation

MathlibNt.SieveTheory.LiLiuGoldbachWeightG11RoughConsumed

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughTotal (N : ℕ) (ε : ℝ) :
ℤ
Equations
Instances For
    Inspect dependencies

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

    source
    noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11RoughRemainder (N : ℕ) (ε : ℝ) :
    ℤ

    Replace only the actual G11 term. No other signed term is changed or estimated.

    Equations
    Instances For
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_le_roughTotal_normalized (δ : ℝ) (hδ : 0 < δ) :
      ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ), 0 ≤ ε → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ ↑(goldbachG11RoughTotal N ε) + δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_g11Rough_consumed_eventually (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) :
      ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (Z : ℝ), 1 ≤ Z → Z ≤ √↑N → ↑(goldbachWeightG11RoughRemainder N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Z) + (goldbachWeightHighFirstCoefficient ε - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

      The rough G11 count and the low-S5 sifted count both remain literal, unestimated counts.

      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_g11Rough_consumed_small_epsilon (δ : ℝ) (hδ : 0 < δ) :
      ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (Z : ℝ), 1 ≤ Z → Z ≤ √↑N → ↑(goldbachWeightG11RoughRemainder N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Z) + (goldbachWeightHighFirstCoefficient 0 - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)
      Inspect dependencies

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