← Mathematical handbook

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

Equations

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

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

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

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

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

theorem Verification.IncreasingBand.density_zero_ae (B : IncreasingBand) : ∀ᵐ (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.IncreasingBand.conditionalDensity (B : IncreasingBand) (p : ↑unitInterval × ↑unitInterval) : ℝ

Equations

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

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

theorem Verification.IncreasingBand.measure_eq_conditional (B : IncreasingBand) : 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.IncreasingBand.standardizedDensity (B : IncreasingBand) (p : ↑unitInterval × ↑unitInterval) : ℝ

Equations

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

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

theorem Verification.IncreasingBand.standardized_law (B : IncreasingBand) : 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.IncreasingBand.copula_density (B : IncreasingBand) : 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.