← Copula mathematical handbook

Coordinate reflections of copulas

def ProbabilityTheory.Copula.reflectPoint {d : ℕ} (s : Finset (Fin d)) (x : Fin d → ↑unitInterval) (i : Fin d) : ↑unitInterval

Reflect exactly the coordinates in s.

Equations

• ProbabilityTheory.Copula.reflectPoint s x i = if i ∈ s then unitInterval.symm (x i) else x i

theorem ProbabilityTheory.Copula.measurable_reflectPoint {d : ℕ} (s : Finset (Fin d)) : Measurable (reflectPoint s)

@[simp]

theorem ProbabilityTheory.Copula.reflectPoint_reflectPoint {d : ℕ} (s : Finset (Fin d)) (x : Fin d → ↑unitInterval) : reflectPoint s (reflectPoint s x) = x

noncomputable def ProbabilityTheory.Copula.reflect {d : ℕ} (C : Copula d) (s : Finset (Fin d)) : Copula d

Uniform marginals are preserved by reflection about 1/2.

Equations

• C.reflect s = ProbabilityTheory.Copula.ofMap C.measure (ProbabilityTheory.Copula.reflectPoint s) ⋯ ⋯

@[simp]

theorem ProbabilityTheory.Copula.toMeasure_reflect {d : ℕ} (C : Copula d) (s : Finset (Fin d)) : (C.reflect s).toMeasure = MeasureTheory.Measure.map (reflectPoint s) C.toMeasure

@[simp]

theorem ProbabilityTheory.Copula.reflect_empty {d : ℕ} (C : Copula d) : C.reflect ∅ = C

@[simp]

theorem ProbabilityTheory.Copula.reflect_reflect {d : ℕ} (C : Copula d) (s : Finset (Fin d)) : (C.reflect s).reflect s = C

Reflection is an involution, including for the empty cube.

theorem ProbabilityTheory.Copula.reflect_injective {d : ℕ} (s : Finset (Fin d)) : Function.Injective fun (C : Copula d) => C.reflect s