← Mathematical handbook

Coordinate transformations

Selecting coordinates preserves copulas. The selection need not be injective: repeating a coordinate is allowed and introduces perfect dependence. Coordinate permutations are a special case.

noncomputable def ProbabilityTheory.Copula.reindex {d e : ℕ} (C : Copula d) (ρ : Fin e → Fin d) : Copula e

Select, reorder, or repeat coordinates of a copula.

Equations

• C.reindex ρ = ProbabilityTheory.Copula.ofMap C.measure (fun (x : Fin d → ↑unitInterval) (i : Fin e) => x (ρ i)) ⋯ ⋯

@[simp]

theorem ProbabilityTheory.Copula.toMeasure_reindex {d e : ℕ} (C : Copula d) (ρ : Fin e → Fin d) : (C.reindex ρ).toMeasure = MeasureTheory.Measure.map (fun (x : Fin d → ↑unitInterval) (i : Fin e) => x (ρ i)) C.toMeasure

@[simp]

theorem ProbabilityTheory.Copula.reindex_id {d : ℕ} (C : Copula d) : C.reindex id = C

theorem ProbabilityTheory.Copula.reindex_reindex {d e f : ℕ} (C : Copula d) (ρ : Fin e → Fin d) (η : Fin f → Fin e) : (C.reindex ρ).reindex η = C.reindex (ρ ∘ η)

@[simp]

theorem ProbabilityTheory.Copula.reindex_equiv_symm {d e : ℕ} (C : Copula d) (ρ : Fin e ≃ Fin d) : (C.reindex ⇑ρ).reindex ⇑ρ.symm = C

Applying a coordinate permutation and its inverse recovers the copula.