theorem G67SumCoordinate.split_integral {l m r : ℝ} {f : ℝ → ℝ} (hlm : l ≤ m) (hmr : m ≤ r) (hf : ContinuousOn f (Set.Icc l r)) : ∫ (s : ℝ) in l..r, f s = (∫ (s : ℝ) in l..m, f s) + ∫ (s : ℝ) in m..r, f s

Split a compact continuous integral at an interior point.

theorem G67SumCoordinate.square_density_continuousOn : ContinuousOn (fun (s : ℝ) => profile s * weight (4 / 53) (4 / 33) (4 / 53) (4 / 33) s) (Set.Icc (4 / 53 + 4 / 53) (4 / 33 + 4 / 33))

Continuity of the actual square density on its full sum interval.

theorem G67SumCoordinate.rectangle_density_continuousOn : ContinuousOn (fun (s : ℝ) => profile s * weight (4 / 53) (4 / 33) (4 / 33) (3 / 11) s) (Set.Icc (4 / 53 + 4 / 33) (4 / 33 + 3 / 11))

Continuity of the actual rectangular density on its full sum interval.

theorem G67SumCoordinate.rectangle_integral_truncate : ∫ (s : ℝ) in 4 / 53 + 4 / 33..4 / 33 + 3 / 11, profile s * weight (4 / 53) (4 / 33) (4 / 33) (3 / 11) s = ∫ (s : ℝ) in 4 / 53 + 4 / 33..1 / 2 - 2 * (4 / 53), profile s * weight (4 / 53) (4 / 33) (4 / 33) (3 / 11) s

Exact removal of the zero tail, not an inequality or a numerical approximation.

noncomputable def G67SumCoordinate.truncatedIntegral : ℝ

The exact one-dimensional auxiliary constant with its identically zero tail removed.

Equations

• G67SumCoordinate.truncatedIntegral = (1 / 2 * ∫ (s : ℝ) in 4 / 53 + 4 / 53..4 / 33 + 4 / 33, G67SumCoordinate.profile s * G67SumCoordinate.weight (4 / 53) (4 / 33) (4 / 53) (4 / 33) s) + ∫ (s : ℝ) in 4 / 53 + 4 / 33..1 / 2 - 2 * (4 / 53), G67SumCoordinate.profile s * G67SumCoordinate.weight (4 / 53) (4 / 33) (4 / 33) (3 / 11) s

theorem G67SumCoordinate.elementaryIntegral_eq_truncated : G67ElementaryIntegral.elementaryIntegral = truncatedIntegral

Unconditional exact equality to the imported original elementary integral.

theorem G67SumCoordinate.actual_constant_lower_truncated : 4 * truncatedIntegral ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67IntegralConstant

Actual C67 consumer after exact tail removal.