Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG67ElementaryIntegralBridge

source
theorem G67ElementaryIntegral.weighted_continuousOn :
ContinuousOn (fun (x : ℝ × ℝ) => elementaryKernel x / (x.1 * x.2)) (Set.Icc (4 / 53) (4 / 33) ×ˢ Set.Icc (4 / 53) (3 / 11))

Continuity on the full compact domain of the two actual integrals.

Inspect dependencies

G67ElementaryIntegral.weighted_continuousOn · compiled type and proof/definition references.

source
theorem G67ElementaryIntegral.weighted_integrable {c d : ℝ} (hc : 4 / 53 ≤ c) (hd : d ≤ 3 / 11) :
MeasureTheory.IntegrableOn (fun (x : ℝ × ℝ) => elementaryKernel x / (x.1 * x.2)) (Set.Ioc (4 / 53) (4 / 33) ×ˢ Set.Ioc c d) MeasureTheory.volume

Actual weighted integrability, with no analytic input premises.

Inspect dependencies

G67ElementaryIntegral.weighted_integrable · compiled type and proof/definition references.

source
theorem G67ElementaryIntegral.rectangle_lower {c d : ℝ} (hc : 4 / 53 ≤ c) (hd : d ≤ 3 / 11) (hcd : c ≤ d) :
2 * Real.exp Real.eulerMascheroniConstant * (4 / 53) * ∫ (u : ℝ) in 4 / 53..4 / 33, ∫ (v : ℝ) in c..d, elementaryKernel (u, v) / (u * v) ≤ ∫ (u : ℝ) in 4 / 53..4 / 33, ∫ (v : ℝ) in c..d, LiLiuGoldbachIdealPairKernel.kernel 0 (u, v) / (u * v)

The pointwise lower bound integrated over either required positive rectangle.

Inspect dependencies

G67ElementaryIntegral.rectangle_lower · compiled type and proof/definition references.

source
noncomputable def G67ElementaryIntegral.elementaryIntegral :
ℝ

A separately named auxiliary integral preserves both original domains and the half-square.

Equations
Instances For
    Inspect dependencies

    G67ElementaryIntegral.elementaryIntegral · compiled type and proof/definition references.

    source
    theorem G67ElementaryIntegral.actual_integral_lower :
    2 * Real.exp Real.eulerMascheroniConstant * (4 / 53) * elementaryIntegral ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67JRIntegral 0

    The actual unnormalized JR integral dominates the explicit auxiliary integral.

    Inspect dependencies

    G67ElementaryIntegral.actual_integral_lower · compiled type and proof/definition references.

    source
    theorem G67ElementaryIntegral.actual_constant_lower :
    4 * elementaryIntegral ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67IntegralConstant

    The fixed actual C67 has the explicit exp-free logarithmic integral lower bound.

    Inspect dependencies

    G67ElementaryIntegral.actual_constant_lower · compiled type and proof/definition references.

    source
    theorem G67ElementaryIntegral.actual_constant_lower_explicit :
    4 * ((1 / 2 * ∫ (u : ℝ) (v : ℝ) in 4 / 53..4 / 33, max 0 (Real.log ((1 / 2 - u - v - 4 / 53) / (4 / 53)) / (1 / 2 - u - v)) / (u * v)) + ∫ (u : ℝ) in 4 / 53..4 / 33, ∫ (v : ℝ) in 4 / 33..3 / 11, max 0 (Real.log ((1 / 2 - u - v - 4 / 53) / (4 / 53)) / (1 / 2 - u - v)) / (u * v)) ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67IntegralConstant

    Literal public endpoint: no JR function, exponential, or analytic premise on the lower side.

    Inspect dependencies

    G67ElementaryIntegral.actual_constant_lower_explicit · compiled type and proof/definition references.