Documentation

MathlibNt.SieveTheory.LiLiuGoldbachS5HighScalarChange

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highU (x : ℝ) :
ℝ
Equations
Instances For
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highU_maps {x : ℝ} (hx : x ∈ Set.Icc 0 (7 / 27)) :
    highU x ∈ Set.Icc (1 / 10) (1 / 3)
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highF_continuous :
    ContinuousOn highF (Set.Icc 0 (7 / 27))
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.high_change_integral :
    goldbachB9HighMainIntegral = ∫ (x : ℝ) in 0..7 / 27, highF x
    Inspect dependencies

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