← Mathematical handbook

Copulas obtained by tagging two conditional models on predictor blocks

noncomputable def Verification.joinKernel (C D : ProbabilityTheory.Copula 2) (a v u : ↑unitInterval) : ℝ

Equations

• Verification.joinKernel C D a v u = Verification.unitJoin a (fun (t : ↑unitInterval) => C.conditionalCDF t v) (fun (t : ↑unitInterval) => D.conditionalCDF t v) u

theorem Verification.joinKernel_measurable (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : Measurable fun (p : ↑unitInterval × ↑unitInterval) => joinKernel C D a p.1 p.2

theorem Verification.joinKernel_mem (C D : ProbabilityTheory.Copula 2) (a v u : ↑unitInterval) : joinKernel C D a v u ∈ Set.Icc 0 1

theorem Verification.joinKernel_integrable (C D : ProbabilityTheory.Copula 2) (a v : ↑unitInterval) : MeasureTheory.Integrable (joinKernel C D a v) MeasureTheory.volume

theorem Verification.joinKernel_mean (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), joinKernel C D a v u = ↑v

theorem Verification.joinKernel_mono (C D : ProbabilityTheory.Copula 2) (a u : ↑unitInterval) : Monotone fun (v : ↑unitInterval) => joinKernel C D a v u

theorem Verification.joinKernel_zero (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : joinKernel C D a 0 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 0

theorem Verification.joinKernel_one (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : joinKernel C D a 1 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 1

noncomputable def Verification.conditionalJoin (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : ProbabilityTheory.Copula 2

Equations

• Verification.conditionalJoin C D a ha0 ha1 = Verification.copulaOfConditionalAE (Verification.joinKernel C D a) ⋯ ⋯ ⋯ ⋯ ⋯

theorem Verification.conditionalJoin_conditionalCDF (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (conditionalJoin C D a ha0 ha1).conditionalCDF u v) =ᵐ[MeasureTheory.volume] joinKernel C D a v