← Copula mathematical handbook

Measure-preserving rearrangements and complete dependence

Coordinatewise uniform-preserving maps transform copulas into copulas. The maps need not be invertible. Invertible maps include generalized shuffles; finite piecewise shuffles are not separately encoded here.

graphCopula f hf is the law of (U, f(U)), for uniform U. Its conditional law is deterministic, and its Markov products follow composition of maps.

noncomputable def ProbabilityTheory.Copula.rearrange {d : ℕ} (C : Copula d) (f : Fin d → ↑unitInterval → ↑unitInterval) (hf : ∀ (i : Fin d), MeasureTheory.MeasurePreserving (f i) MeasureTheory.volume MeasureTheory.volume) : Copula d

Apply a uniform-preserving map to each coordinate of a copula.

Equations

• C.rearrange f hf = ProbabilityTheory.Copula.ofMap C.measure (fun (x : Fin d → ↑unitInterval) (i : Fin d) => f i (x i)) ⋯ ⋯

@[simp]

theorem ProbabilityTheory.Copula.toMeasure_rearrange {d : ℕ} (C : Copula d) (f : Fin d → ↑unitInterval → ↑unitInterval) (hf : ∀ (i : Fin d), MeasureTheory.MeasurePreserving (f i) MeasureTheory.volume MeasureTheory.volume) : (C.rearrange f hf).toMeasure = MeasureTheory.Measure.map (fun (x : Fin d → ↑unitInterval) (i : Fin d) => f i (x i)) C.toMeasure

@[simp]

theorem ProbabilityTheory.Copula.rearrange_id {d : ℕ} (C : Copula d) : C.rearrange (fun (x : Fin d) => id) ⋯ = C

theorem ProbabilityTheory.Copula.rearrange_rearrange {d : ℕ} (C : Copula d) (f g : Fin d → ↑unitInterval → ↑unitInterval) (hf : ∀ (i : Fin d), MeasureTheory.MeasurePreserving (f i) MeasureTheory.volume MeasureTheory.volume) (hg : ∀ (i : Fin d), MeasureTheory.MeasurePreserving (g i) MeasureTheory.volume MeasureTheory.volume) : (C.rearrange f hf).rearrange g hg = C.rearrange (fun (i : Fin d) => g i ∘ f i) ⋯

theorem ProbabilityTheory.Copula.rearrange_inverse {d : ℕ} (C : Copula d) (f g : Fin d → ↑unitInterval → ↑unitInterval) (hf : ∀ (i : Fin d), MeasureTheory.MeasurePreserving (f i) MeasureTheory.volume MeasureTheory.volume) (hg : ∀ (i : Fin d), MeasureTheory.MeasurePreserving (g i) MeasureTheory.volume MeasureTheory.volume) (hgf : ∀ (i : Fin d), Function.LeftInverse (g i) (f i)) : (C.rearrange f hf).rearrange g hg = C

Inverse rearrangements recover the original copula.

@[simp]

theorem ProbabilityTheory.Copula.rearrange_independence {d : ℕ} (f : Fin d → ↑unitInterval → ↑unitInterval) (hf : ∀ (i : Fin d), MeasureTheory.MeasurePreserving (f i) MeasureTheory.volume MeasureTheory.volume) : (independence d).rearrange f hf = independence d

def ProbabilityTheory.Copula.IsCompletelyDependent (C : Copula 2) : Prop

Complete dependence: the second coordinate is a measurable function of the first.

Equations

• C.IsCompletelyDependent = ∃ (f : ↑unitInterval → ↑unitInterval), Measurable f ∧ ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 1 = f (x 0)

def ProbabilityTheory.Copula.IsMutuallyCompletelyDependent (C : Copula 2) : Prop

Mutual complete dependence requires functional dependence in both directions.

Equations

• C.IsMutuallyCompletelyDependent = (C.IsCompletelyDependent ∧ C.transpose.IsCompletelyDependent)

noncomputable def ProbabilityTheory.Copula.graphCopula (f : ↑unitInterval → ↑unitInterval) (hf : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) : Copula 2

The copula of a uniform variable and a uniform-preserving function of it.

Equations

• ProbabilityTheory.Copula.graphCopula f hf = ProbabilityTheory.Copula.ofMap ⟨MeasureTheory.volume, ProbabilityTheory.Copula.graphCopula._proof_1⟩ (fun (u : ↑unitInterval) => ![u, f u]) ⋯ ⋯

@[simp]

theorem ProbabilityTheory.Copula.toMeasure_graphCopula (f : ↑unitInterval → ↑unitInterval) (hf : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) : (graphCopula f hf).toMeasure = MeasureTheory.Measure.map (fun (u : ↑unitInterval) => ![u, f u]) MeasureTheory.volume

theorem ProbabilityTheory.Copula.ae_graphCopula (f : ↑unitInterval → ↑unitInterval) (hf : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(graphCopula f hf).toMeasure, x 1 = f (x 0)

theorem ProbabilityTheory.Copula.isCompletelyDependent_graphCopula (f : ↑unitInterval → ↑unitInterval) (hf : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) : (graphCopula f hf).IsCompletelyDependent

theorem ProbabilityTheory.Copula.conditionalKernel_graphCopula (f : ↑unitInterval → ↑unitInterval) (hf : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) : ⇑(graphCopula f hf).conditionalKernel =ᵐ[MeasureTheory.volume] ⇑(Kernel.deterministic f ⋯)

theorem ProbabilityTheory.Copula.measurePreserving_of_ae_function (C : Copula 2) {f : ↑unitInterval → ↑unitInterval} (hf : Measurable f) (h : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 1 = f (x 0)) : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume

A functional response in a copula automatically preserves uniform volume.

theorem ProbabilityTheory.Copula.eq_graphCopula_of_ae_function (C : Copula 2) {f : ↑unitInterval → ↑unitInterval} (hf : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) (h : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 1 = f (x 0)) : C = graphCopula f hf

theorem ProbabilityTheory.Copula.isCompletelyDependent_iff (C : Copula 2) : C.IsCompletelyDependent ↔ ∃ (f : ↑unitInterval → ↑unitInterval) (hf : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume), C = graphCopula f hf

theorem ProbabilityTheory.Copula.IsCompletelyDependent.chatterjeeXi_eq_one {C : Copula 2} (h : C.IsCompletelyDependent) : C.chatterjeeXi = 1

theorem ProbabilityTheory.Copula.IsCompletelyDependent.copulaCorrelationRatio_eq_one {C : Copula 2} (h : C.IsCompletelyDependent) : C.copulaCorrelationRatio = 1

@[simp]

theorem ProbabilityTheory.Copula.graphCopula_id : graphCopula id ⋯ = comonotonic 2

@[simp]

theorem ProbabilityTheory.Copula.graphCopula_symm : graphCopula unitInterval.symm unitInterval.measurePreserving_symm = countermonotonic

theorem ProbabilityTheory.Copula.markovProduct_graphCopula (f g : ↑unitInterval → ↑unitInterval) (hf : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) (hg : MeasureTheory.MeasurePreserving g MeasureTheory.volume MeasureTheory.volume) : (graphCopula f hf).markovProduct (graphCopula g hg) = graphCopula (g ∘ f) ⋯

For deterministic transitions, the product follows ordinary function composition.

noncomputable def ProbabilityTheory.Copula.shuffle (C : Copula 2) (e : ↑unitInterval ≃ᵐ ↑unitInterval) (he : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.volume MeasureTheory.volume) : Copula 2

A generalized shuffle acts on the second coordinate by a uniform-preserving measurable bijection. In contrast, rearrange also allows noninvertible maps.

Equations

• C.shuffle e he = C.rearrange ![id, ⇑e] ⋯

theorem ProbabilityTheory.Copula.toMeasure_shuffle (C : Copula 2) (e : ↑unitInterval ≃ᵐ ↑unitInterval) (he : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.volume MeasureTheory.volume) : (C.shuffle e he).toMeasure = MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) => ![x 0, e (x 1)]) C.toMeasure

@[simp]

theorem ProbabilityTheory.Copula.shuffle_symm (C : Copula 2) (e : ↑unitInterval ≃ᵐ ↑unitInterval) (he : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.volume MeasureTheory.volume) : (C.shuffle e he).shuffle e.symm ⋯ = C

@[simp]

theorem ProbabilityTheory.Copula.shuffle_independence (e : ↑unitInterval ≃ᵐ ↑unitInterval) (he : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.volume MeasureTheory.volume) : (independence 2).shuffle e he = independence 2

@[simp]

theorem ProbabilityTheory.Copula.shuffle_comonotonic (e : ↑unitInterval ≃ᵐ ↑unitInterval) (he : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.volume MeasureTheory.volume) : (comonotonic 2).shuffle e he = graphCopula (⇑e) he

theorem ProbabilityTheory.Copula.transpose_graphCopula (e : ↑unitInterval ≃ᵐ ↑unitInterval) (he : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.volume MeasureTheory.volume) : (graphCopula (⇑e) he).transpose = graphCopula ⇑e.symm ⋯

theorem ProbabilityTheory.Copula.isMutuallyCompletelyDependent_graphCopula (e : ↑unitInterval ≃ᵐ ↑unitInterval) (he : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.volume MeasureTheory.volume) : (graphCopula (⇑e) he).IsMutuallyCompletelyDependent

theorem ProbabilityTheory.Copula.isMutuallyCompletelyDependent_shuffle_comonotonic (e : ↑unitInterval ≃ᵐ ↑unitInterval) (he : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.volume MeasureTheory.volume) : ((comonotonic 2).shuffle e he).IsMutuallyCompletelyDependent

A generalized shuffle of Min is mutually completely dependent.

@[simp]

theorem ProbabilityTheory.Copula.countermonotonic_markovProduct_countermonotonic : countermonotonic.markovProduct countermonotonic = comonotonic 2

@[simp]

theorem ProbabilityTheory.Copula.shuffle_reflection (C : Copula 2) : C.shuffle unitInterval.symmMeasurableEquiv ⋯ = C.reflect {1}

A shuffle by the interval reflection recovers the existing copula reflection.