← Mathematical handbook

Propositions 2 and 4(ii): absolute continuity and an MTP2 density

theorem Papers.AnsariRockel2026XiRho.sourceBandDensity_integrable {b : ℝ} (hb : 0 < b) : MeasureTheory.Integrable (sourceBandDensity b) MeasureTheory.volume

theorem Papers.AnsariRockel2026XiRho.sourceBandDensity_cdf {b : ℝ} (hb : 0 < b) (u : Fin 2 → ↑unitInterval) : ∫ (x : Fin 2 → ↑unitInterval) in Set.Iic u, sourceBandDensity b x = (sourceBand b hb).cdf u

Integrating the density over every lower orthant gives the original source CDF.

theorem Papers.AnsariRockel2026XiRho.sourceBand_toMeasure_density (b : ℝ) (hb : 0 < b) : (sourceBand b hb).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (sourceBandDensity b x)

This is an equality of probability measures, not a pointwise candidate density.

theorem Papers.AnsariRockel2026XiRho.sourceBand_absolutelyContinuous (b : ℝ) (hb : 0 < b) : (sourceBand b hb).toMeasure.AbsolutelyContinuous MeasureTheory.volume

Proposition 2: the entire positive source family is absolutely continuous.

theorem Papers.AnsariRockel2026XiRho.sourceBandDensity_isMTP2 {b : ℝ} (hb : 0 < b) : ProbabilityTheory.IsMTP2 (sourceBandDensity b)

The support's increasing interval endpoints imply total positivity of the density.

theorem Papers.AnsariRockel2026XiRho.sourceBand_hasMTP2Density (b : ℝ) (hb : 0 < b) : (sourceBand b hb).HasMTP2Density

Proposition 4(ii), with an actual nonnegative measurable Lebesgue density.