← Mathematical handbook

theorem Verification.map_withDensity_comp {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) {T : X → Y} (hT : Measurable T) {h : Y → ENNReal} (hh : Measurable h) : MeasureTheory.Measure.map T (μ.withDensity (h ∘ T)) = (MeasureTheory.Measure.map T μ).withDensity h

Pushforward of a density that factors through the measurable map.

noncomputable def Verification.ExclusionBand.marginal (B : ExclusionBand) : MeasureTheory.Measure ↑unitInterval

Equations

• B.marginal = MeasureTheory.Measure.map Prod.snd B.measure

instance Verification.ExclusionBand.instIsProbabilityMeasureElemRealUnitIntervalMarginal (B : ExclusionBand) : MeasureTheory.IsProbabilityMeasure B.marginal

instance Verification.ExclusionBand.instNullSingletonClassElemRealUnitIntervalMarginal (B : ExclusionBand) : MeasureTheory.NullSingletonClass B.marginal

theorem Verification.ExclusionBand.marginal_real (B : ExclusionBand) : MeasureTheory.Measure.map Subtype.val B.marginal = B.secondLaw

theorem Verification.ExclusionBand.marginal_cdf (B : ExclusionBand) (t : ↑unitInterval) : unitCDF B.marginal t = ProbabilityTheory.cdfUnit B.secondLaw ↑t

theorem Verification.ExclusionBand.density_zero_ae (B : ExclusionBand) : ∀ᵐ (p : ↑unitInterval × ↑unitInterval), B.columnDensity p.2 = 0 → B.density p = 0

The numerator vanishes almost everywhere on zero-density marginal fibers.

noncomputable def Verification.ExclusionBand.conditionalDensity (B : ExclusionBand) (p : ↑unitInterval × ↑unitInterval) : ℝ

Equations

• B.conditionalDensity p = B.density p / B.columnDensity p.2

theorem Verification.ExclusionBand.conditionalDensity_measurable (B : ExclusionBand) : Measurable B.conditionalDensity

theorem Verification.ExclusionBand.measure_eq_conditional (B : ExclusionBand) : B.measure = (MeasureTheory.volume.prod B.marginal).withDensity fun (p : ↑unitInterval × ↑unitInterval) => ENNReal.ofReal (B.conditionalDensity p)

Disintegration as a density relative to the product of the two marginals.

noncomputable def Verification.ExclusionBand.standardizedDensity (B : ExclusionBand) (p : ↑unitInterval × ↑unitInterval) : ℝ

Equations

• B.standardizedDensity p = B.conditionalDensity (p.1, ProbabilityTheory.unitQuantile B.marginal p.2)

theorem Verification.ExclusionBand.standardizedDensity_measurable (B : ExclusionBand) : Measurable B.standardizedDensity

theorem Verification.ExclusionBand.standardizedDensity_eq (B : ExclusionBand) (p : ↑unitInterval × ↑unitInterval) : B.standardizedDensity p = if B.lower p.1 ≤ ↑(ProbabilityTheory.unitQuantile B.marginal p.2) ∧ ↑(ProbabilityTheory.unitQuantile B.marginal p.2) ≤ B.lower p.1 + B.width then 0 else 1 / ((1 - B.width) * B.columnDensity (ProbabilityTheory.unitQuantile B.marginal p.2))

Equation (32), as a pointwise formula with the usual zero convention for division.

theorem Verification.ExclusionBand.standardized_law (B : ExclusionBand) : MeasureTheory.Measure.map (fun (p : ↑unitInterval × ↑unitInterval) => (p.1, unitCDF B.marginal p.2)) B.measure = MeasureTheory.volume.withDensity fun (p : ↑unitInterval × ↑unitInterval) => ENNReal.ofReal (B.standardizedDensity p)

Standardization really has the displayed density, even when the marginal has flat intervals.

theorem Verification.ExclusionBand.copula_density (B : ExclusionBand) : B.copula.toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (B.standardizedDensity (x 0, x 1))

The copula measure itself, in the package's two-coordinate representation.

theorem Verification.ExclusionBand.copula_raw_density (B : ExclusionBand) (hm : B.marginal = MeasureTheory.volume) : B.copula.toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (B.density (x 0, x 1))

When the second marginal is already uniform, standardization changes no values.

theorem Verification.ExclusionBand.measure_eq_volume_of_width_zero (B : ExclusionBand) (hw : B.width = 0) : B.measure = MeasureTheory.volume

A zero-width excluded graph has product measure zero.

theorem Verification.ExclusionBand.copula_eq_independence_of_width_zero (B : ExclusionBand) (hw : B.width = 0) : B.copula = ProbabilityTheory.Copula.independence 2