← Mathematical handbook

noncomputable def Verification.IncreasingBand.columnDensity (B : IncreasingBand) (v : ↑unitInterval) : ℝ

Equations

• B.columnDensity v = ∫ (u : ↑unitInterval), B.density (u, v)

theorem Verification.IncreasingBand.columnDensity_measurable (B : IncreasingBand) : Measurable B.columnDensity

theorem Verification.IncreasingBand.columnDensity_nonneg (B : IncreasingBand) (v : ↑unitInterval) : 0 ≤ B.columnDensity v

theorem Verification.IncreasingBand.columnDensity_integrable (B : IncreasingBand) : MeasureTheory.Integrable B.columnDensity MeasureTheory.volume

theorem Verification.IncreasingBand.columnDensity_integral (B : IncreasingBand) : ∫ (v : ↑unitInterval), B.columnDensity v = 1

theorem Verification.IncreasingBand.map_snd (B : IncreasingBand) : MeasureTheory.Measure.map Prod.snd B.measure = MeasureTheory.volume.withDensity fun (v : ↑unitInterval) => ENNReal.ofReal (B.columnDensity v)

The second marginal law is exactly the density obtained by integrating rows.