← Mathematical handbook

Products of copulas with coordinatewise power weights

For independent vectors U ~ C, V ~ D, the coordinatewise maximum of Uᵢ^(1/aᵢ) and Vᵢ^(1/(1-aᵢ)) is uniform in each coordinate. Zero weights are represented by a constant zero sample, so both endpoints are included.

noncomputable def ProbabilityTheory.Copula.maxProductPoint {d : ℕ} (a : Fin d → ↑unitInterval) (p : (Fin d → ↑unitInterval) × (Fin d → ↑unitInterval)) (i : Fin d) : ↑unitInterval

The maximum of two independent vectors with complementary power marginal laws.

Equations

• ProbabilityTheory.Copula.maxProductPoint a p i = max (ProbabilityTheory.Copula.powerSample (a i) (p.1 i)) (ProbabilityTheory.Copula.powerSample (unitInterval.symm (a i)) (p.2 i))

theorem ProbabilityTheory.Copula.measurable_maxProductPoint {d : ℕ} (a : Fin d → ↑unitInterval) : Measurable (maxProductPoint a)

noncomputable def ProbabilityTheory.Copula.maxProduct {d : ℕ} (C D : Copula d) (a : Fin d → ↑unitInterval) : Copula d

The Liebscher power-product construction for two copulas.

Equations

• C.maxProduct D a = ProbabilityTheory.Copula.ofMap ⟨C.toMeasure.prod D.toMeasure, ⋯⟩ (ProbabilityTheory.Copula.maxProductPoint a) ⋯ ⋯

theorem ProbabilityTheory.Copula.cdf_maxProduct {d : ℕ} (C D : Copula d) (a u : Fin d → ↑unitInterval) : (C.maxProduct D a).cdf u = (C.cdf fun (i : Fin d) => unitPower (u i) ↑(a i) ⋯) * D.cdf fun (i : Fin d) => unitPower (u i) ↑(unitInterval.symm (a i)) ⋯

@[simp]

theorem ProbabilityTheory.Copula.maxProduct_zero {d : ℕ} (C D : Copula d) : (C.maxProduct D fun (x : Fin d) => 0) = D

@[simp]

theorem ProbabilityTheory.Copula.maxProduct_one {d : ℕ} (C D : Copula d) : (C.maxProduct D fun (x : Fin d) => 1) = C