Documentation

MathlibNt.SieveTheory.LiLiuGoldbachS3IntegralScalarAnalytic

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3eval :
List ℚ → ℝ → ℝ

Dense exact rational polynomial, in increasing coefficient order.

Equations
Instances For
    Inspect dependencies

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

    source
    noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3primAux :
    List ℚ → ℕ → ℝ → ℝ

    A rational primitive; the natural offset makes the derivative induction transparent.

    Equations
    Instances For
      Inspect dependencies

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

      source
      noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3prim (cs : List ℚ) :
      ℝ → ℝ
      Equations
      Instances For
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3eval_continuous (cs : List ℚ) :
        Continuous (s3eval cs)
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3primAux_hasDerivAt (cs : List ℚ) (n : ℕ) (x : ℝ) :
        HasDerivAt (s3primAux cs n) (x ^ n * s3eval cs x) x
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3prim_hasDerivAt (cs : List ℚ) (x : ℝ) :
        HasDerivAt (s3prim cs) (s3eval cs x) x
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3geom_lower {x : ℝ} (hx : 0 ≤ x) (h1 : x < 1) (n : ℕ) :
        ∑ k ∈ Finset.range n, x ^ k ≤ 1 / (1 - x)

        Finite geometric lower bound, valid on the entire interval.

        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3geom_upper {x : ℝ} (hx : 0 ≤ x) (hu : x ≤ 3 / 5) :
        1 / (1 - x) ≤ ∑ k ∈ Finset.range 64, x ^ k + 5 / 2 * (3 / 5) ^ 64

        Fixed-order geometric upper bound, with uniform analytic remainder.

        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3change_kernel {s : ℝ} (hs : s ∈ Set.Icc 3 (45 / 8)) :
        53 / (s * (53 / 8 - s)) = (-8 / (3 - (s - 3) / (s - 1)) + 360 / (29 - 45 * ((s - 3) / (s - 1)))) * (2 / (s - 1) ^ 2)

        The exact transformed Jacobian-kernel identity.

        Inspect dependencies

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