MathlibNt.SieveTheory.LiLiuGoldbachG12AnalyticEnvelope

source

noncomputable def G12AnalyticCertificate.upperDensity (u : ℝ) :

ℝ

The source degree-33 logarithmic envelope, with both inverse powers retained.

Equations

G12AnalyticCertificate.upperDensity u = (1 / (4 / 33) + (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L (4 / 33 / u - 1) - 1) / u) / u

Instances For

Inspect dependencies

G12AnalyticCertificate.upperDensity · compiled type and proof/definition references.

source

theorem G12AnalyticCertificate.density_le_upperDensity {u : ℝ} (hu : u ∈ Set.Icc (4 / 53) (4 / 33)) :

G12SharpQuadrature.density u ≤ upperDensity u

This bound is pointwise on the whole original interval, not sampled.

Inspect dependencies

G12AnalyticCertificate.density_le_upperDensity · compiled type and proof/definition references.

source

theorem G12AnalyticCertificate.density_nonneg {u : ℝ} (hu : u ∈ Set.Icc (4 / 53) (4 / 33)) :

0 ≤ G12SharpQuadrature.density u

Positivity is needed before replacing the external logarithmic factor.

Inspect dependencies

G12AnalyticCertificate.density_nonneg · compiled type and proof/definition references.

source

theorem G12AnalyticCertificate.continuousOn_upperDensity :

ContinuousOn upperDensity (Set.Icc (4 / 53) (4 / 33))

Inspect dependencies

G12AnalyticCertificate.continuousOn_upperDensity · compiled type and proof/definition references.

source

theorem G12AnalyticCertificate.low_continuous (f : ℝ → ℝ) (hf : ContinuousOn f (Set.Icc (4 / 53) (4 / 33))) :

ContinuousOn (fun (u : ℝ) => f u / (1 - u)) (Set.Icc (4 / 53) (1 / 10))

Inspect dependencies

G12AnalyticCertificate.low_continuous · compiled type and proof/definition references.

source

noncomputable def G12AnalyticCertificate.upperMass :

ℝ

A logarithm-free rational-function upper integral; the original low factor is retained.

Equations

G12AnalyticCertificate.upperMass = (561990 / 1000000 * (36 / 5) * ∫ (u : ℝ) in 4 / 53..1 / 10, G12AnalyticCertificate.upperDensity u / (1 - u)) + 564383 / 1000000 * 8 * ∫ (u : ℝ) in 1 / 10..4 / 33, G12AnalyticCertificate.upperDensity u

Instances For

Inspect dependencies

G12AnalyticCertificate.upperMass · compiled type and proof/definition references.

source

theorem G12AnalyticCertificate.upperMass_nonneg :

0 ≤ upperMass

Inspect dependencies

G12AnalyticCertificate.upperMass_nonneg · compiled type and proof/definition references.

source

theorem G12AnalyticCertificate.sharp_le_log_mul_upperMass :

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12SharpIntegralConstant ≤ Real.log (9 / 4) * upperMass

Direct consumption of the production sharp split; no mother mass is reconstructed.

Inspect dependencies

G12AnalyticCertificate.sharp_le_log_mul_upperMass · compiled type and proof/definition references.

source

theorem G12AnalyticCertificate.external_log_le :

Real.log (9 / 4) ≤ 2 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L (1 / 2)

Inspect dependencies

G12AnalyticCertificate.external_log_le · compiled type and proof/definition references.

source

theorem G12AnalyticCertificate.sharp_le_rationalIntegral :

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12SharpIntegralConstant ≤ 2 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L (1 / 2) * upperMass

Unconditional analytic upper bound, with no logarithms in its defining integrands.

Inspect dependencies

G12AnalyticCertificate.sharp_le_rationalIntegral · compiled type and proof/definition references.