MathlibNt.SieveTheory.LiLiuGoldbachG67CenteredPolynomial

noncomputable def G67Centered.a :

Fixed analytic polynomial candidate. None of the approximation estimates or the target coefficient is asserted by these definitions.

Equations

G67Centered.a = 4 / 53

Instances For

Inspect dependencies

G67Centered.a · compiled type and proof/definition references.

source

noncomputable def G67Centered.b :

ℝ

Equations

G67Centered.b = 4 / 33

Instances For

Inspect dependencies

G67Centered.b · compiled type and proof/definition references.

source

noncomputable def G67Centered.c :

ℝ

Equations

G67Centered.c = 3 / 11

Instances For

Inspect dependencies

G67Centered.c · compiled type and proof/definition references.

source

noncomputable def G67Centered.cutoff :

ℝ

Equations

G67Centered.cutoff = 1 / 2 - 2 * G67Centered.a

Instances For

Inspect dependencies

G67Centered.cutoff · compiled type and proof/definition references.

source

noncomputable def G67Centered.center :

ℝ

Equations

G67Centered.center = (G67Centered.a + G67Centered.c) / 2

Instances For

Inspect dependencies

G67Centered.center · compiled type and proof/definition references.

source

noncomputable def G67Centered.profilePolynomial (s : ℝ) :

ℝ

Equations

G67Centered.profilePolynomial s = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower (37 / 16) + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L ((1 / 2 - s - G67Centered.a) / G67Centered.a / (37 / 16) - 1)

Instances For

Inspect dependencies

G67Centered.profilePolynomial · compiled type and proof/definition references.

source

noncomputable def G67Centered.shiftedLogPolynomial (t s : ℝ) :

ℝ

Equations

G67Centered.shiftedLogPolynomial t s = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L ((s - t) / G67Centered.center - 1)

Instances For

Inspect dependencies

G67Centered.shiftedLogPolynomial · compiled type and proof/definition references.

source

noncomputable def G67Centered.squareEarly (s : ℝ) :

ℝ

Equations

G67Centered.squareEarly s = 2 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower (G67Centered.center / G67Centered.a) + 2 * G67Centered.shiftedLogPolynomial G67Centered.a s

Instances For

Inspect dependencies

G67Centered.squareEarly · compiled type and proof/definition references.

source

noncomputable def G67Centered.squareLate (s : ℝ) :

ℝ

Equations

G67Centered.squareLate s = 2 * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower (2 * G67Centered.b / G67Centered.center) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logUpper 2) - 2 * G67Centered.shiftedLogPolynomial G67Centered.b s

Instances For

Inspect dependencies

G67Centered.squareLate · compiled type and proof/definition references.

source

noncomputable def G67Centered.rectangleEarly (s : ℝ) :

ℝ

Equations

G67Centered.rectangleEarly s = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower (G67Centered.center ^ 2 / (G67Centered.a * G67Centered.b)) + G67Centered.shiftedLogPolynomial G67Centered.b s + G67Centered.shiftedLogPolynomial G67Centered.a s

Instances For

Inspect dependencies

G67Centered.rectangleEarly · compiled type and proof/definition references.

source

noncomputable def G67Centered.rectangleMiddle (s : ℝ) :

ℝ

Equations

G67Centered.rectangleMiddle s = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower (G67Centered.b / G67Centered.a) + G67Centered.shiftedLogPolynomial G67Centered.a s - G67Centered.shiftedLogPolynomial G67Centered.b s

Instances For

Inspect dependencies

G67Centered.rectangleMiddle · compiled type and proof/definition references.

source

noncomputable def G67Centered.rectangleLate (s : ℝ) :

ℝ

Equations

G67Centered.rectangleLate s = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower (G67Centered.b * G67Centered.c / G67Centered.center ^ 2) - G67Centered.shiftedLogPolynomial G67Centered.c s - G67Centered.shiftedLogPolynomial G67Centered.b s

Instances For

Inspect dependencies

G67Centered.rectangleLate · compiled type and proof/definition references.

source

def G67Centered.reciprocalPolynomial (s : ℝ) :

ℝ

Fixed geometric polynomial for 1/(s*(1/2-s)), centered at 1/4.

Equations

G67Centered.reciprocalPolynomial s = 16 * ∑ k ∈ Finset.range 16, ((4 * s - 1) ^ 2) ^ k

Instances For

Inspect dependencies

G67Centered.reciprocalPolynomial · compiled type and proof/definition references.

source

noncomputable def G67Centered.densityPolynomial (w : ℝ → ℝ) (s : ℝ) :

ℝ

Equations

G67Centered.densityPolynomial w s = G67Centered.profilePolynomial s * w s * G67Centered.reciprocalPolynomial s

Instances For

Inspect dependencies

G67Centered.densityPolynomial · compiled type and proof/definition references.

source

noncomputable def G67Centered.polynomialIntegral :

ℝ

Equations

Instances For

Inspect dependencies

G67Centered.polynomialIntegral · compiled type and proof/definition references.

source

noncomputable def G67Centered.errorBudget :

ℝ

Candidate uniform density loss times the exact weighted interval length. Its sufficiency must be proved separately, not inferred from this name.

Equations

G67Centered.errorBudget = (G67Centered.cutoff - 2 * G67Centered.a) / 40000

Instances For

Inspect dependencies

G67Centered.errorBudget · compiled type and proof/definition references.