Documentation

MathlibNt.SieveTheory.LiLiuGoldbachPositiveScalarValues

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarL (z : ℝ) :
ℝ

The one fixed log truncation; its degree is not selected by a search.

Equations
Instances For
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarL_bounds {z : ℝ} (hz : 0 ≤ z) (hzu : z ≤ 2 / 3) :
    goldbachPositiveScalarL z ≤ Real.log ((1 + z) / (1 - z)) ∧ Real.log ((1 + z) / (1 - z)) ≤ goldbachPositiveScalarL z + 1 / 10 ^ 9

    Uniform analytic log error on the complete closed transformed interval.

    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalar_actual_eq :
    goldbachWeightFiveNegativeScalarCoefficient = 53 / 2 * (Real.log 5 + ∫ (v : ℝ) in 3..5, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) + 8 * (Real.log (25 / 8) + ∫ (v : ℝ) in 3..25 / 8, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) - 2360636 / 100000 - 1951976 / 100000 - 4 * (84289 / 100000) - 540996 / 100000 - 2 * (60962 / 100000)

    Source identification for the literal f(6), f(33/8), not f(53/8).

    Inspect dependencies

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

    source
    noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarExactRational :
    ℝ

    The fixed exact rational analytic expression, prior to decimal rounding.

    Equations
    Instances For
      Inspect dependencies

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

      source
      noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarRationalLower :
      ℝ

      Single downward rounding of the fixed exact expression to denominator 10^8.

      Equations
      Instances For
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalar_rounding :
        goldbachPositiveScalarRationalLower ≤ goldbachPositiveScalarExactRational ∧ goldbachPositiveScalarExactRational < goldbachPositiveScalarRationalLower + 1 / 10 ^ 8

        Kernel-checked exact rational comparison; no approximate evaluation is used.

        Inspect dependencies

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