theorem G67CenteredEnvelope.g67CenteredEnvelope_constants_pos : 0 < G67Centered.a ∧ 0 < G67Centered.b ∧ 0 < G67Centered.c ∧ 0 < G67Centered.center

Positivity certificates shared by the centered logarithmic bounds.

theorem G67CenteredEnvelope.shifted_error {t s : ℝ} (h : s - t ∈ Set.Icc G67Centered.a G67Centered.c) : |G67Centered.shiftedLogPolynomial t s - Real.log ((s - t) / G67Centered.center)| ≤ 1 / 10000000

theorem G67CenteredEnvelope.profile_error {s : ℝ} (hs : s ∈ Set.Icc (2 * G67Centered.a) G67Centered.cutoff) : |G67Centered.profilePolynomial s - Real.log ((1 / 2 - s - G67Centered.a) / G67Centered.a)| ≤ 11 / 100000000

theorem G67CenteredEnvelope.log_product_center {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : Real.log (x * y / (G67Centered.a * G67Centered.b)) = Real.log (G67Centered.center ^ 2 / (G67Centered.a * G67Centered.b)) + Real.log (x / G67Centered.center) + Real.log (y / G67Centered.center)

noncomputable def G67CenteredEnvelope.squareEarlyArgument (s : ℝ) : ℝ

Equations

• G67CenteredEnvelope.squareEarlyArgument s = (s - G67Centered.a) * (s - G67Centered.a) / (G67Centered.a * G67Centered.a)

theorem G67CenteredEnvelope.squareEarly_bounds {s : ℝ} (hs : s ∈ Set.Icc (2 * G67Centered.a) (G67Centered.a + G67Centered.b)) : |G67Centered.squareEarly s - Real.log (squareEarlyArgument s)| ≤ 22 / 100000000 ∧ |Real.log (squareEarlyArgument s)| ≤ 2

noncomputable def G67CenteredEnvelope.squareLateArgument (s : ℝ) : ℝ

Equations

• G67CenteredEnvelope.squareLateArgument s = G67Centered.b * G67Centered.b / ((s - G67Centered.b) * (s - G67Centered.b))

theorem G67CenteredEnvelope.squareLate_bounds {s : ℝ} (hs : s ∈ Set.Icc (G67Centered.a + G67Centered.b) (2 * G67Centered.b)) : |G67Centered.squareLate s - Real.log (squareLateArgument s)| ≤ 22 / 100000000 ∧ |Real.log (squareLateArgument s)| ≤ 2

noncomputable def G67CenteredEnvelope.rectangleEarlyArgument (s : ℝ) : ℝ

Equations

• G67CenteredEnvelope.rectangleEarlyArgument s = (s - G67Centered.b) * (s - G67Centered.a) / (G67Centered.a * G67Centered.b)

theorem G67CenteredEnvelope.rectangleEarly_bounds {s : ℝ} (hs : s ∈ Set.Icc (G67Centered.a + G67Centered.b) (2 * G67Centered.b)) : |G67Centered.rectangleEarly s - Real.log (rectangleEarlyArgument s)| ≤ 22 / 100000000 ∧ |Real.log (rectangleEarlyArgument s)| ≤ 2

noncomputable def G67CenteredEnvelope.rectangleMiddleArgument (s : ℝ) : ℝ

Equations

• G67CenteredEnvelope.rectangleMiddleArgument s = G67Centered.b * (s - G67Centered.a) / (G67Centered.a * (s - G67Centered.b))

theorem G67CenteredEnvelope.rectangleMiddle_bounds {s : ℝ} (hs : s ∈ Set.Icc (2 * G67Centered.b) (G67Centered.a + G67Centered.c)) : |G67Centered.rectangleMiddle s - Real.log (rectangleMiddleArgument s)| ≤ 22 / 100000000 ∧ |Real.log (rectangleMiddleArgument s)| ≤ 2

noncomputable def G67CenteredEnvelope.rectangleLateArgument (s : ℝ) : ℝ

Equations

• G67CenteredEnvelope.rectangleLateArgument s = G67Centered.b * G67Centered.c / ((s - G67Centered.c) * (s - G67Centered.b))

theorem G67CenteredEnvelope.rectangleLate_bounds {s : ℝ} (hs : s ∈ Set.Icc (G67Centered.a + G67Centered.c) G67Centered.cutoff) : |G67Centered.rectangleLate s - Real.log (rectangleLateArgument s)| ≤ 22 / 100000000 ∧ |Real.log (rectangleLateArgument s)| ≤ 2

theorem G67CenteredEnvelope.density_bridge {s : ℝ} (hs : s ∈ Set.Icc (2 * G67Centered.a) G67Centered.cutoff) {w : ℝ → ℝ} {W : ℝ} (hw : |w s - W| ≤ 22 / 100000000) (hW : |W| ≤ 3) : G67Centered.densityPolynomial w s - 1 / 40000 ≤ G67SumCoordinate.profile s * (W / s)

The max in the actual profile is removed only on the certified full active interval.

theorem G67CenteredEnvelope.continuous_densityPolynomial {w : ℝ → ℝ} (hw : Continuous w) : Continuous (G67Centered.densityPolynomial w)

theorem G67CenteredEnvelope.integrate_loss {l u : ℝ} {f g : ℝ → ℝ} (hlu : l ≤ u) (hf : Continuous f) (hg : ContinuousOn g (Set.Icc l u)) (h : ∀ s ∈ Set.Icc l u, f s - 1 / 40000 ≤ g s) : (∫ (s : ℝ) in l..u, f s) - (u - l) / 40000 ≤ ∫ (s : ℝ) in l..u, g s

Integrate a signed pointwise density loss; no polynomial sign hypothesis is used.