Documentation

Copula.Dependence.Conditional

← Mathematical handbook

Conditional kernels as witnesses of stochastic increasingness #

source
theorem ProbabilityTheory.Copula.cdf_eq_integral_conditionalCDF (C : Copula 2) (u v : ↑unitInterval) :
C.cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, C.conditionalCDF t v

Disintegration along the first coordinate recovers the copula CDF.

source
theorem ProbabilityTheory.Copula.cdf_eq_integral_kernel (C : Copula 2) (κ : Kernel ↑unitInterval ↑unitInterval) (hκ : ⇑C.conditionalKernel =ᵐ[MeasureTheory.volume] ⇑κ) (u v : ↑unitInterval) :
C.cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, (κ t).real (Set.Iic v)
source
theorem ProbabilityTheory.Copula.integral_Iic_add_Ioc_unit {f : ↑unitInterval → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) {a b : ↑unitInterval} (hab : a ≤ b) :
(∫ (t : ↑unitInterval) in Set.Iic a, f t) + ∫ (t : ↑unitInterval) in Set.Ioc a b, f t = ∫ (t : ↑unitInterval) in Set.Iic b, f t
source
theorem ProbabilityTheory.Copula.integral_Iic_concave_of_antitone {f : ↑unitInterval → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (ha : Antitone f) (a b c : ↑unitInterval) (hab : a ≤ b) (hbc : b ≤ c) :
((↑b - ↑a) * ∫ (t : ↑unitInterval) in Set.Iic c, f t) + (↑c - ↑b) * ∫ (t : ↑unitInterval) in Set.Iic a, f t ≤ (↑c - ↑a) * ∫ (t : ↑unitInterval) in Set.Iic b, f t

The indefinite integral of an antitone function satisfies the concavity chord inequality.

source
theorem ProbabilityTheory.Copula.isSI_of_kernel (C : Copula 2) (κ : Kernel ↑unitInterval ↑unitInterval) [IsMarkovKernel κ] (hκ : ⇑C.conditionalKernel =ᵐ[MeasureTheory.volume] ⇑κ) (hmono : ∀ (v : ↑unitInterval), Antitone fun (u : ↑unitInterval) => (κ u).real (Set.Iic v)) :
C.IsSI

A stochastically increasing version of the conditional kernel proves SI. The almost-everywhere identification makes this independent of null-set choices.

source
def ProbabilityTheory.Copula.HasTP2Kernel (C : Copula 2) :
Prop

TP2 of a version of the conditional CDF kernel. This allows singular copulas.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ProbabilityTheory.Copula.HasTP2Kernel.isSI {C : Copula 2} (h : C.HasTP2Kernel) :
    C.IsSI