Documentation

Verification.ConditionalBlocks

← Mathematical handbook

Affine localization of two conditional models into diagonal blocks #

source
noncomputable def Verification.blockKernel (C D : ProbabilityTheory.Copula 2) (a v u : ↑unitInterval) :
ℝ
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Verification.blockKernel_measurable (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) :
    Measurable fun (p : ↑unitInterval × ↑unitInterval) => blockKernel C D a p.1 p.2
    source
    theorem Verification.blockKernel_mem (C D : ProbabilityTheory.Copula 2) (a v u : ↑unitInterval) :
    blockKernel C D a v u ∈ Set.Icc 0 1
    source
    theorem Verification.blockKernel_integrable (C D : ProbabilityTheory.Copula 2) (a v : ↑unitInterval) :
    MeasureTheory.Integrable (blockKernel C D a v) MeasureTheory.volume
    source
    theorem Verification.blockKernel_mean (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (v : ↑unitInterval) :
    ∫ (u : ↑unitInterval), blockKernel C D a v u = ↑v
    source
    theorem Verification.blockKernel_mono (C D : ProbabilityTheory.Copula 2) (a u : ↑unitInterval) :
    Monotone fun (v : ↑unitInterval) => blockKernel C D a v u
    source
    theorem Verification.blockKernel_zero (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) :
    blockKernel C D a 0 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 0
    source
    theorem Verification.blockKernel_one (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) :
    blockKernel C D a 1 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 1
    source
    noncomputable def Verification.conditionalBlocks (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) :
    ProbabilityTheory.Copula 2
    Equations
    Instances For
      source
      theorem Verification.conditionalBlocks_conditionalCDF (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (v : ↑unitInterval) :
      (fun (u : ↑unitInterval) => (conditionalBlocks C D a ha0 ha1).conditionalCDF u v) =ᵐ[MeasureTheory.volume] blockKernel C D a v
      source
      theorem Verification.conditionalMean_conditionalBlocks (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) :
      conditionalMean (conditionalBlocks C D a ha0 ha1) =ᵐ[MeasureTheory.volume] unitJoin a (fun (u : ↑unitInterval) => ↑a * conditionalMean C u) fun (u : ↑unitInterval) => ↑a + (1 - ↑a) * conditionalMean D u