← Copula mathematical handbook

Constructing a copula from a family of conditional CDFs

theorem ProbabilityTheory.Copula.RankRegion.Common.conditional_integral_classical (h : ↑unitInterval → ↑unitInterval → ℝ) (hi : ∀ (v : ↑unitInterval), MeasureTheory.Integrable (h v) MeasureTheory.volume) (hm : ∀ (u : ↑unitInterval), Monotone fun (v : ↑unitInterval) => h v u) (hz : ∀ (u : ↑unitInterval), h 0 u = 0) (ho : ∀ (u : ↑unitInterval), h 1 u = 1) (hmean : ∀ (v : ↑unitInterval), ∫ (u : ↑unitInterval), h v u = ↑v) : IsClassical fun (z : Fin 2 → ↑unitInterval) => ∫ (u : ↑unitInterval) in Set.Iic (z 0), h (z 1) u

Integral construction, with uniform mean and monotonicity in the response threshold.

noncomputable def ProbabilityTheory.Copula.RankRegion.Common.copulaOfConditional (h : ↑unitInterval → ↑unitInterval → ℝ) (hi : ∀ (v : ↑unitInterval), MeasureTheory.Integrable (h v) MeasureTheory.volume) (hm : ∀ (u : ↑unitInterval), Monotone fun (v : ↑unitInterval) => h v u) (hz : ∀ (u : ↑unitInterval), h 0 u = 0) (ho : ∀ (u : ↑unitInterval), h 1 u = 1) (hmean : ∀ (v : ↑unitInterval), ∫ (u : ↑unitInterval), h v u = ↑v) : Copula 2

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.Common.copulaOfConditional_cdf (h : ↑unitInterval → ↑unitInterval → ℝ) (hi : ∀ (v : ↑unitInterval), MeasureTheory.Integrable (h v) MeasureTheory.volume) (hm : ∀ (u : ↑unitInterval), Monotone fun (v : ↑unitInterval) => h v u) (hz : ∀ (u : ↑unitInterval), h 0 u = 0) (ho : ∀ (u : ↑unitInterval), h 1 u = 1) (hmean : ∀ (v : ↑unitInterval), ∫ (u : ↑unitInterval), h v u = ↑v) (u v : ↑unitInterval) : (copulaOfConditional h hi hm hz ho hmean).cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, h v t

theorem ProbabilityTheory.Copula.RankRegion.Common.copulaOfConditional_kernel (h : ↑unitInterval → ↑unitInterval → ℝ) (hi : ∀ (v : ↑unitInterval), MeasureTheory.Integrable (h v) MeasureTheory.volume) (hm : ∀ (u : ↑unitInterval), Monotone fun (v : ↑unitInterval) => h v u) (hz : ∀ (u : ↑unitInterval), h 0 u = 0) (ho : ∀ (u : ↑unitInterval), h 1 u = 1) (hmean : ∀ (v : ↑unitInterval), ∫ (u : ↑unitInterval), h v u = ↑v) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (copulaOfConditional h hi hm hz ho hmean).conditionalCDF u v) =ᵐ[MeasureTheory.volume] h v