noncomputable def G12SharpQuadrature.density (u : ℝ) : ℝ

The exact single-variable density of the four-variable cross.

Equations

• G12SharpQuadrature.density u = (1 / (4 / 33) + (Real.log (4 / 33 / u) - 1) / u) / u

theorem G12SharpQuadrature.continuousOn_density : ContinuousOn density (Set.Icc (4 / 53) (4 / 33))

theorem G12SharpQuadrature.integrable_weighted (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) : IntervalIntegrable (fun (u : ℝ) => h u * density u) MeasureTheory.volume (4 / 53) (4 / 33)

theorem G12SharpQuadrature.integral_eq_density (h : ℝ → ℝ) : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral h = Real.log (9 / 4) * ∫ (u : ℝ) in 4 / 53..4 / 33, h u * density u

theorem G12SharpQuadrature.sharp_low {u : ℝ} (hu : u < 1 / 10) : G12SharpWeight.weight u = 561990 / 1000000 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight u

theorem G12SharpQuadrature.sharp_high {u : ℝ} (hu : 1 / 10 ≤ u) : G12SharpWeight.weight u = 564383 / 1000000 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight u

theorem G12SharpQuadrature.sharp_mul_integrable (g : ℝ → ℝ) (hg : ContinuousOn g (Set.Icc (4 / 53) (4 / 33))) : IntervalIntegrable (fun (u : ℝ) => G12SharpWeight.weight u * g u) MeasureTheory.volume (4 / 53) (4 / 33)

Multiplication by a continuous density preserves sharp-weight integrability.

theorem G12SharpQuadrature.sharp_weight_intervalIntegrable : IntervalIntegrable G12SharpWeight.weight MeasureTheory.volume (4 / 53) (4 / 33)

Integrability of the original discontinuous weight itself.

theorem G12SharpQuadrature.sharp_integrable : IntervalIntegrable (fun (u : ℝ) => G12SharpWeight.weight u * density u) MeasureTheory.volume (4 / 53) (4 / 33)

Integrability of the discontinuous sharp weighted density, proved branchwise.

theorem G12SharpQuadrature.sharp_integral_split : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral G12SharpWeight.weight = Real.log (9 / 4) * ((561990 / 1000000 * (36 / 5) * ∫ (u : ℝ) in 4 / 53..1 / 10, density u / (1 - u)) + 564383 / 1000000 * 8 * ∫ (u : ℝ) in 1 / 10..4 / 33, density u)

Endpoint removal occurs only inside Lebesgue integrals, never in the prime sum.

theorem G12SharpQuadrature.sharp_outer_intervalIntegrable : IntervalIntegrable (fun (r : ℝ) => ∫ (q : ℝ) in r..4 / 33, ∫ (s : ℝ) in q..4 / 33, ∫ (t : ℝ) in 4 / 33..3 / 11, G12SharpWeight.weight r / (r * q ^ 2 * s * t)) MeasureTheory.volume (4 / 53) (4 / 33)

The discontinuous weight also gives an integrable literal outer cross slice.