Documentation

Verification.ConditionalCopula

← Mathematical handbook

Constructing a copula from a family of conditional CDFs #

source
theorem Verification.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) :
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.

source
noncomputable def Verification.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) :
ProbabilityTheory.Copula 2
Equations
Instances For
    source
    theorem Verification.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
    source
    theorem Verification.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