Documentation

MathlibNt.SieveTheory.LiLiuGoldbachWeightRemainingSix

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

The six literal signed terms after both S3 terms. No sign or main estimate is assumed for this remaining integer-valued expression.

Equations
Instances For
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightRemainingEight_eq_remainingSix_sub_s3Pair (A : Finset ℕ) (N : ℕ) (z b c : ℝ) :
    goldbachWeightRemainingEight A N z b c = goldbachWeightRemainingSix A N z b c - goldbachS3Closed A N z (↑N ^ (1 / 3)) - goldbachS3Closed A N z c
    Inspect dependencies

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

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

    Each S3 term has external multiplicity one, not the S2 multiplicity four.

    Equations
    Instances For
      Inspect dependencies

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

      source
      @[simp]
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightSixCoefficient_zero :
      goldbachWeightSixCoefficient 0 = goldbachWeightKnownCoefficient 0 - 53 / 2 * Real.exp (-Real.eulerMascheroniConstant) * (goldbachS3_primeKernelIntegral (1 / 3) + goldbachS3_primeKernelIntegral (3 / 11))
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightSixCoefficient_continuousAt_zero :
      ContinuousAt goldbachWeightSixCoefficient 0
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightSixCoefficient_small_epsilon (η : ℝ) (hη : 0 < η) :
      ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → |goldbachWeightSixCoefficient ε - goldbachWeightSixCoefficient 0| < η

      The scalar coefficient can be frozen at zero only after choosing epsilon; this theorem itself makes no assertion about a count or its positivity.

      Inspect dependencies

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