Documentation

MathlibNt.SieveTheory.LiLiuGoldbachWeightRemainingFive

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightRemainingFive (A : Finset ℕ) (N : ℕ) (z b c : ℝ) :
ℤ

The five literal signed terms, after consumption of the externally doubled S4.

Equations
Instances For
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightRemainingSix_eq_remainingFive_sub_two_s4 (A : Finset ℕ) (N : ℕ) (z b c : ℝ) :
    goldbachWeightRemainingSix A N z b c = goldbachWeightRemainingFive A N z b c - 2 * goldbachS4 A N c
    Inspect dependencies

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

    source
    noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightFiveCoefficient (ε : ℝ) :
    ℝ

    The coefficient includes the external factor two: 2*(8I8)=16I8.

    Equations
    Instances For
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_remainingFive_S1_S2_S3_S4_I10_consumed_eventually (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) :
      ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightRemainingFive (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) + (goldbachWeightFiveCoefficient ε - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

      The actual S4 integral bound is consumed, without a sign assumption on the five remaining terms.

      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_remainingFive_small_epsilon (δ : ℝ) (hδ : 0 < δ) :
      ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightRemainingFive (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) + (goldbachWeightFiveCoefficient 0 - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

      The small-epsilon quantifiers remain epsilon0 first, then a threshold for each epsilon.

      Inspect dependencies

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