← Mathematical handbook

noncomputable def Verification.ExclusionBand.holeLength (B : ExclusionBand) (v : ↑unitInterval) : ℝ

Equations

• B.holeLength v = ∫ (u : ↑unitInterval), if B.lower u ≤ ↑v ∧ ↑v ≤ B.lower u + B.width then 1 else 0

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

Equations

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

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

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

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

theorem Verification.ExclusionBand.columnDensity_eq (B : ExclusionBand) (v : ↑unitInterval) : B.columnDensity v = (1 - B.holeLength v) / (1 - B.width)

Equation (31): the actual second-coordinate density.

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

theorem Verification.ExclusionBand.map_snd (B : ExclusionBand) : 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.