Documentation

Copula.MarkovProduct

← Copula mathematical handbook

Bistochastic kernels and the Markov product #

A Markov kernel preserving uniform volume determines a bivariate copula. Composing these kernels defines the Darsow–Nguyen–Olsen Markov product: C.markovProduct D follows first the transition of C, then that of D. All constructions include singular copulas and are independent of null-set choices of conditional kernels.

noncomputable def ProbabilityTheory.Copula.ofKernel (κ : Kernel ↑unitInterval ↑unitInterval) [IsMarkovKernel κ] (hκ : MeasureTheory.volume.bind ⇑κ = MeasureTheory.volume) :

Construct a copula from a Markov kernel that preserves uniform volume.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem ProbabilityTheory.Copula.toMeasure_ofKernel (κ : Kernel ↑unitInterval ↑unitInterval) [IsMarkovKernel κ] (hκ : MeasureTheory.volume.bind ⇑κ = MeasureTheory.volume) :

(ofKernel κ hκ).toMeasure = MeasureTheory.Measure.map (fun (p : ↑unitInterval × ↑unitInterval) => ![p.1, p.2]) (MeasureTheory.volume.compProd κ)

theorem ProbabilityTheory.Copula.map_pair_ofKernel (κ : Kernel ↑unitInterval ↑unitInterval) [IsMarkovKernel κ] (hκ : MeasureTheory.volume.bind ⇑κ = MeasureTheory.volume) :

MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) => (x 0, x 1)) (ofKernel κ hκ).toMeasure = MeasureTheory.volume.compProd κ

theorem ProbabilityTheory.Copula.conditionalKernel_ofKernel (κ : Kernel ↑unitInterval ↑unitInterval) [IsMarkovKernel κ] (hκ : MeasureTheory.volume.bind ⇑κ = MeasureTheory.volume) :

⇑(ofKernel κ hκ).conditionalKernel =ᵐ[MeasureTheory.volume] ⇑κ

theorem ProbabilityTheory.Copula.ofKernel_congr {κ η : Kernel ↑unitInterval ↑unitInterval} [IsMarkovKernel κ] [IsMarkovKernel η] (hκ : MeasureTheory.volume.bind ⇑κ = MeasureTheory.volume) (hη : MeasureTheory.volume.bind ⇑η = MeasureTheory.volume) (h : ⇑κ =ᵐ[MeasureTheory.volume] ⇑η) :

ofKernel κ hκ = ofKernel η hη

@[simp]

theorem ProbabilityTheory.Copula.ofKernel_conditionalKernel (C : Copula 2) :

ofKernel C.conditionalKernel ⋯ = C

theorem ProbabilityTheory.Copula.eq_of_conditionalKernel_ae_eq {C D : Copula 2} (h : ⇑C.conditionalKernel =ᵐ[MeasureTheory.volume] ⇑D.conditionalKernel) :

C = D

A copula is determined by its conditional kernel up to uniform-null sets.

theorem ProbabilityTheory.Copula.conditionalKernel_comonotonic :

⇑(comonotonic 2).conditionalKernel =ᵐ[MeasureTheory.volume] ⇑Kernel.id

noncomputable def ProbabilityTheory.Copula.markovProduct (C D : Copula 2) :

The Markov product follows C and then D, with the middle coordinate integrated out. Independence is absorbing and comonotonicity is the identity.

Equations

C.markovProduct D = ProbabilityTheory.Copula.ofKernel (D.conditionalKernel.comp C.conditionalKernel) ⋯

Instances For

theorem ProbabilityTheory.Copula.conditionalKernel_markovProduct (C D : Copula 2) :

⇑(C.markovProduct D).conditionalKernel =ᵐ[MeasureTheory.volume] ⇑(D.conditionalKernel.comp C.conditionalKernel)

theorem ProbabilityTheory.Copula.cdf_markovProduct (C D : Copula 2) (u v : ↑unitInterval) :

(C.markovProduct D).cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, ((D.conditionalKernel.comp C.conditionalKernel) t).real (Set.Iic v)

The CDF of the product, in a kernel form valid without densities.

theorem ProbabilityTheory.Copula.kernel_comp_ae_congr_left (C : Copula 2) {κ η : Kernel ↑unitInterval ↑unitInterval} (h : ⇑κ =ᵐ[MeasureTheory.volume] ⇑η) :

⇑(κ.comp C.conditionalKernel) =ᵐ[MeasureTheory.volume] ⇑(η.comp C.conditionalKernel)

Compose almost-everywhere equal kernels on the left of a uniform-preserving transition.

theorem ProbabilityTheory.Copula.markovProduct_assoc (C D E : Copula 2) :

(C.markovProduct D).markovProduct E = C.markovProduct (D.markovProduct E)

@[simp]

theorem ProbabilityTheory.Copula.markovProduct_comonotonic (C : Copula 2) :

C.markovProduct (comonotonic 2) = C

@[simp]

theorem ProbabilityTheory.Copula.comonotonic_markovProduct (C : Copula 2) :

(comonotonic 2).markovProduct C = C

@[simp]

theorem ProbabilityTheory.Copula.markovProduct_independence (C : Copula 2) :

C.markovProduct (independence 2) = independence 2

@[simp]

theorem ProbabilityTheory.Copula.independence_markovProduct (C : Copula 2) :

(independence 2).markovProduct C = independence 2