← Mathematical handbook

The source density height integrates to its explicit intercept

noncomputable def Papers.AnsariRockel2026XiRho.sourceBandHeight (b : ℝ) (v : ↑unitInterval) : ℝ

Equations

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

theorem Papers.AnsariRockel2026XiRho.sourceBandHeight_nonneg {b : ℝ} (hb : 0 < b) (v : ↑unitInterval) : 0 ≤ sourceBandHeight b v

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

theorem Papers.AnsariRockel2026XiRho.sourceBandHeight_primitive {b : ℝ} (hb : 0 < b) (v : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic v, sourceBandHeight b t = sourceBandIntercept b v

Integrating the proposed density height recovers the source intercept at every threshold.