← Mathematical handbook

Identifying every conditional section of the band density

theorem Papers.AnsariRockel2026XiRho.sourceBandIntercept_mem {b : ℝ} (hb : 0 < b) (v : ↑unitInterval) : sourceBandIntercept b v ∈ Set.Icc 0 (b + 1)

theorem Papers.AnsariRockel2026XiRho.sourceBandIntercept_eq_normalized {b : ℝ} (hb : 0 < b) (v : ↑unitInterval) : sourceBandIntercept b v = Verification.bandIntercept b ⋯ v

theorem Papers.AnsariRockel2026XiRho.sourceBandIntercept_strictMono {b : ℝ} (hb : 0 < b) : StrictMono (sourceBandIntercept b)

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

A density version including the upper band edge; its value on that null edge is immaterial.

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.AnsariRockel2026XiRho.sourceBandDensity_nonneg {b : ℝ} (hb : 0 < b) (x : Fin 2 → ↑unitInterval) : 0 ≤ sourceBandDensity b x

theorem Papers.AnsariRockel2026XiRho.sourceBandDensity_le_height {b : ℝ} (hb : 0 < b) (x : Fin 2 → ↑unitInterval) : sourceBandDensity b x ≤ sourceBandHeight b (x 1)

theorem Papers.AnsariRockel2026XiRho.sourceBandDensity_measurable {b : ℝ} (hb : 0 < b) : Measurable (sourceBandDensity b)

theorem Papers.AnsariRockel2026XiRho.sourceBandDensity_section {b : ℝ} (hb : 0 < b) (u v : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic v, sourceBandDensity b ![u, t] = Verification.unitClamp (sourceBandIntercept b v - b * ↑u)

Integrating the density in the response rank gives exactly the source conditional CDF.