Documentation

Verification.ConditionalLawRealization

← Mathematical handbook

Realizing a law of conditional laws by a copula #

source
noncomputable def Verification.copulaOfKernel (κ : ProbabilityTheory.Kernel ↑unitInterval ↑unitInterval) [ProbabilityTheory.IsMarkovKernel κ] (hκ : MeasureTheory.volume.bind ⇑κ = MeasureTheory.volume) :
ProbabilityTheory.Copula 2

A Markov kernel preserving the uniform law defines a copula.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Verification.copulaOfKernel_conditional (κ : ProbabilityTheory.Kernel ↑unitInterval ↑unitInterval) [ProbabilityTheory.IsMarkovKernel κ] (hκ : MeasureTheory.volume.bind ⇑κ = MeasureTheory.volume) :
    ⇑(copulaOfKernel κ hκ).conditionalKernel =ᵐ[MeasureTheory.volume] ⇑κ

    Its selected conditional kernel is the original kernel almost everywhere.

    source
    theorem Verification.exists_copula_conditionalLaw (Λ : MeasureTheory.ProbabilityMeasure (MeasureTheory.ProbabilityMeasure ↑unitInterval)) (hΛ : Λ ∈ uniformBarycenter) :
    ∃ (C : ProbabilityTheory.Copula 2), conditionalLaw C = Λ

    Every law of probability measures with uniform barycenter is realized by a copula.