← Mathematical handbook

Constructing a copula from a family of conditional CDFs

theorem Verification.conditional_integral_classical_ae (h : ↑unitInterval → ↑unitInterval → ℝ) (hi : ∀ (v : ↑unitInterval), MeasureTheory.Integrable (h v) MeasureTheory.volume) (hm : ∀ (u : ↑unitInterval), Monotone fun (v : ↑unitInterval) => h v u) (hz : h 0 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 0) (ho : h 1 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 1) (hmean : ∀ (v : ↑unitInterval), ∫ (u : ↑unitInterval), h v u = ↑v) : ProbabilityTheory.Copula.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 Verification.copulaOfConditionalAE (h : ↑unitInterval → ↑unitInterval → ℝ) (hi : ∀ (v : ↑unitInterval), MeasureTheory.Integrable (h v) MeasureTheory.volume) (hm : ∀ (u : ↑unitInterval), Monotone fun (v : ↑unitInterval) => h v u) (hz : h 0 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 0) (ho : h 1 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 1) (hmean : ∀ (v : ↑unitInterval), ∫ (u : ↑unitInterval), h v u = ↑v) : ProbabilityTheory.Copula 2

Equations

• Verification.copulaOfConditionalAE h hi hm hz ho hmean = ProbabilityTheory.Copula.ofClassical (fun (z : Fin 2 → ↑unitInterval) => ∫ (u : ↑unitInterval) in Set.Iic (z 0), h (z 1) u) ⋯

theorem Verification.copulaOfConditionalAE_cdf (h : ↑unitInterval → ↑unitInterval → ℝ) (hi : ∀ (v : ↑unitInterval), MeasureTheory.Integrable (h v) MeasureTheory.volume) (hm : ∀ (u : ↑unitInterval), Monotone fun (v : ↑unitInterval) => h v u) (hz : h 0 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 0) (ho : h 1 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 1) (hmean : ∀ (v : ↑unitInterval), ∫ (u : ↑unitInterval), h v u = ↑v) (u v : ↑unitInterval) : (copulaOfConditionalAE h hi hm hz ho hmean).cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, h v t

theorem Verification.copulaOfConditionalAE_kernel (h : ↑unitInterval → ↑unitInterval → ℝ) (hi : ∀ (v : ↑unitInterval), MeasureTheory.Integrable (h v) MeasureTheory.volume) (hm : ∀ (u : ↑unitInterval), Monotone fun (v : ↑unitInterval) => h v u) (hz : h 0 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 0) (ho : h 1 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 1) (hmean : ∀ (v : ↑unitInterval), ∫ (u : ↑unitInterval), h v u = ↑v) (hn : ∀ (v u : ↑unitInterval), 0 ≤ h v u) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (copulaOfConditionalAE h hi hm hz ho hmean).conditionalCDF u v) =ᵐ[MeasureTheory.volume] h v