← Copula mathematical handbook

Conditional quantiles for pair-copula constructions

The generalized inverse of a copula's conditional distribution is jointly measurable and samples its second coordinate given its first. No density or strict monotonicity assumption is needed.

noncomputable def ProbabilityTheory.Copula.conditionalCDFUnit (C : Copula 2) (u v : ↑unitInterval) : ↑unitInterval

The conditional CDF, with its value bundled in the unit interval.

Equations

• C.conditionalCDFUnit u v = ⟨C.conditionalCDF u v, ⋯⟩

noncomputable def ProbabilityTheory.Copula.conditionalQuantile (C : Copula 2) (u t : ↑unitInterval) : ↑unitInterval

The generalized conditional quantile of coordinate 1 given coordinate 0.

Equations

• C.conditionalQuantile u t = ProbabilityTheory.unitQuantile (C.conditionalKernel u) t

theorem ProbabilityTheory.Copula.conditionalQuantile_le_iff (C : Copula 2) (u t v : ↑unitInterval) : C.conditionalQuantile u t ≤ v ↔ t ≤ C.conditionalCDFUnit u v

theorem ProbabilityTheory.Copula.monotone_conditionalQuantile (C : Copula 2) (u : ↑unitInterval) : Monotone (C.conditionalQuantile u)

theorem ProbabilityTheory.Copula.measurable_conditionalQuantile (C : Copula 2) : Measurable (Function.uncurry C.conditionalQuantile)

@[simp]

theorem ProbabilityTheory.Copula.map_conditionalQuantile (C : Copula 2) (u : ↑unitInterval) : MeasureTheory.Measure.map (C.conditionalQuantile u) MeasureTheory.volume = C.conditionalKernel u

theorem ProbabilityTheory.Copula.map_pair_conditionalQuantile (C : Copula 2) : MeasureTheory.Measure.map (fun (p : ↑unitInterval × ↑unitInterval) => ![p.1, C.conditionalQuantile p.1 p.2]) (MeasureTheory.volume.prod MeasureTheory.volume) = C.toMeasure

Conditional inverse-transform sampling recovers the entire bivariate law.

theorem ProbabilityTheory.Copula.map_uncurry_conditionalQuantile (C : Copula 2) : MeasureTheory.Measure.map (Function.uncurry C.conditionalQuantile) (MeasureTheory.volume.prod MeasureTheory.volume) = MeasureTheory.volume

Averaging the conditional quantile over an independent uniform root is uniform.