Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG12EvaluationFTC

source
theorem G12AnalyticCertificate.low_composed_deriv (u : ℝ) (hu : 0 < u) (hb : u ≤ 4 / 33) :
HasDerivAt (fun (u : ℝ) => -lowF (4 / 33 / u - 1)) (upperDensity u / (1 - u)) u
Inspect dependencies

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

source
theorem G12AnalyticCertificate.high_composed_deriv (u : ℝ) (hu : 0 < u) (hb : u ≤ 4 / 33) :
HasDerivAt (fun (u : ℝ) => -highF (4 / 33 / u - 1)) (upperDensity u) u
Inspect dependencies

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

source
theorem G12AnalyticCertificate.low_upper_integral_exact :
∫ (u : ℝ) in 4 / 53..1 / 10, upperDensity u / (1 - u) = lowF (20 / 33) - lowF (7 / 33)
Inspect dependencies

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

source
theorem G12AnalyticCertificate.high_upper_integral_exact :
∫ (u : ℝ) in 1 / 10..4 / 33, upperDensity u = highF (7 / 33) - highF 0
Inspect dependencies

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

source
noncomputable def G12AnalyticCertificate.endpoints :
ℝ
Equations
Instances For
    Inspect dependencies

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

    source
    theorem G12AnalyticCertificate.upperMass_eq_endpoints :
    upperMass = endpoints
    Inspect dependencies

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