← Mathematical handbook

The density of the negative branch

noncomputable def Papers.AnsariRockel2026XiRho.negativeSourceBandDensity (b : ℝ) (x : Fin 2 → ↑unitInterval) : ℝ

The exact reflected open-band density in Remark 3(c).

Equations

• Papers.AnsariRockel2026XiRho.negativeSourceBandDensity b x = Papers.AnsariRockel2026XiRho.sourceBandDensityOpen b (ProbabilityTheory.Copula.reflectPoint {0} x)

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

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

theorem Papers.AnsariRockel2026XiRho.negativeSourceBandDensity_formula (b : ℝ) (x : Fin 2 → ↑unitInterval) : negativeSourceBandDensity b x = if b * (1 - ↑(x 0)) < sourceBandIntercept b (x 1) ∧ sourceBandIntercept b (x 1) < b * (1 - ↑(x 0)) + 1 then sourceBandHeight b (x 1) else 0