Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG67CenteredBridge

source
theorem G67CenteredEnvelope.squareEarly_integral_loss :
(∫ (s : ℝ) in 2 * G67Centered.a..G67Centered.a + G67Centered.b, G67Centered.densityPolynomial G67Centered.squareEarly s) - (G67Centered.a + G67Centered.b - 2 * G67Centered.a) / 40000 ≤ ∫ (s : ℝ) in 2 * G67Centered.a..G67Centered.a + G67Centered.b, G67SumCoordinate.profile s * (Real.log (squareEarlyArgument s) / s)
Inspect dependencies

G67CenteredEnvelope.squareEarly_integral_loss · compiled type and proof/definition references.

source
theorem G67CenteredEnvelope.squareLate_integral_loss :
(∫ (s : ℝ) in G67Centered.a + G67Centered.b..2 * G67Centered.b, G67Centered.densityPolynomial G67Centered.squareLate s) - (2 * G67Centered.b - (G67Centered.a + G67Centered.b)) / 40000 ≤ ∫ (s : ℝ) in G67Centered.a + G67Centered.b..2 * G67Centered.b, G67SumCoordinate.profile s * (Real.log (squareLateArgument s) / s)
Inspect dependencies

G67CenteredEnvelope.squareLate_integral_loss · compiled type and proof/definition references.

source
theorem G67CenteredEnvelope.rectangleEarly_integral_loss :
(∫ (s : ℝ) in G67Centered.a + G67Centered.b..2 * G67Centered.b, G67Centered.densityPolynomial G67Centered.rectangleEarly s) - (2 * G67Centered.b - (G67Centered.a + G67Centered.b)) / 40000 ≤ ∫ (s : ℝ) in G67Centered.a + G67Centered.b..2 * G67Centered.b, G67SumCoordinate.profile s * (Real.log (rectangleEarlyArgument s) / s)
Inspect dependencies

G67CenteredEnvelope.rectangleEarly_integral_loss · compiled type and proof/definition references.

source
theorem G67CenteredEnvelope.rectangleMiddle_integral_loss :
(∫ (s : ℝ) in 2 * G67Centered.b..G67Centered.a + G67Centered.c, G67Centered.densityPolynomial G67Centered.rectangleMiddle s) - (G67Centered.a + G67Centered.c - 2 * G67Centered.b) / 40000 ≤ ∫ (s : ℝ) in 2 * G67Centered.b..G67Centered.a + G67Centered.c, G67SumCoordinate.profile s * (Real.log (rectangleMiddleArgument s) / s)
Inspect dependencies

G67CenteredEnvelope.rectangleMiddle_integral_loss · compiled type and proof/definition references.

source
theorem G67CenteredEnvelope.rectangleLate_integral_loss :
(∫ (s : ℝ) in G67Centered.a + G67Centered.c..G67Centered.cutoff, G67Centered.densityPolynomial G67Centered.rectangleLate s) - (G67Centered.cutoff - (G67Centered.a + G67Centered.c)) / 40000 ≤ ∫ (s : ℝ) in G67Centered.a + G67Centered.c..G67Centered.cutoff, G67SumCoordinate.profile s * (Real.log (rectangleLateArgument s) / s)
Inspect dependencies

G67CenteredEnvelope.rectangleLate_integral_loss · compiled type and proof/definition references.

source
theorem G67CenteredEnvelope.weighted_length :
1 / 2 * (G67Centered.a + G67Centered.b - 2 * G67Centered.a + (2 * G67Centered.b - (G67Centered.a + G67Centered.b))) + (2 * G67Centered.b - (G67Centered.a + G67Centered.b) + (G67Centered.a + G67Centered.c - 2 * G67Centered.b) + (G67Centered.cutoff - (G67Centered.a + G67Centered.c))) = G67Centered.cutoff - 2 * G67Centered.a

The exact weighted length includes the half-square and all three rectangle branches.

Inspect dependencies

G67CenteredEnvelope.weighted_length · compiled type and proof/definition references.

source
theorem G67CenteredEnvelope.errorBudget_value :
G67Centered.errorBudget = 21 / 4240000
Inspect dependencies

G67CenteredEnvelope.errorBudget_value · compiled type and proof/definition references.

source
theorem G67CenteredEnvelope.polynomialIntegral_sub_errorBudget_le_piecewiseIntegral :
G67Centered.polynomialIntegral - G67Centered.errorBudget ≤ G67SumCoordinate.piecewiseIntegral

The unconditional real analytic bridge for the unchanged frozen candidate.

Inspect dependencies

G67CenteredEnvelope.polynomialIntegral_sub_errorBudget_le_piecewiseIntegral · compiled type and proof/definition references.