← Mathematical handbook

Laws of conditional distributions with a uniform barycenter

def Verification.lawKernel : ProbabilityTheory.Kernel (MeasureTheory.ProbabilityMeasure ↑unitInterval) ↑unitInterval

Evaluation turns a probability law into a Markov kernel.

Equations

• Verification.lawKernel = { toFun := MeasureTheory.ProbabilityMeasure.toMeasure, measurable' := Verification.lawKernel._proof_1 }

instance Verification.instIsMarkovKernelProbabilityMeasureElemRealUnitIntervalLawKernel : ProbabilityTheory.IsMarkovKernel lawKernel

def Verification.uniformBarycenter : Set (MeasureTheory.ProbabilityMeasure (MeasureTheory.ProbabilityMeasure ↑unitInterval))

Laws of conditional laws whose averaged response distribution is uniform.

Equations

• Verification.uniformBarycenter = {Λ : MeasureTheory.ProbabilityMeasure (MeasureTheory.ProbabilityMeasure ↑unitInterval) | (↑Λ).bind ⇑Verification.lawKernel = MeasureTheory.volume}

theorem Verification.uniformBarycenter_iff (Λ : MeasureTheory.ProbabilityMeasure (MeasureTheory.ProbabilityMeasure ↑unitInterval)) : Λ ∈ uniformBarycenter ↔ ∀ (f : C(↑unitInterval, ℝ)), ∫ (μ : MeasureTheory.ProbabilityMeasure ↑unitInterval), ∫ (x : ↑unitInterval), f x ∂↑μ ∂↑Λ = ∫ (x : ↑unitInterval), f x

theorem Verification.isCompact_uniformBarycenter : IsCompact uniformBarycenter

Admissible laws form a compact set in the weak topology on laws of laws.

noncomputable def Verification.conditionalLaw (C : ProbabilityTheory.Copula 2) : MeasureTheory.ProbabilityMeasure (MeasureTheory.ProbabilityMeasure ↑unitInterval)

The distribution, under the uniform conditioning variable, of the conditional law.

Equations

• Verification.conditionalLaw C = MeasureTheory.ProbabilityMeasure.map ⟨MeasureTheory.volume, Verification.conditionalLaw._proof_1⟩ fun (u : ↑unitInterval) => ⟨C.conditionalKernel u, ⋯⟩

theorem Verification.measurable_conditionalLawMap (C : ProbabilityTheory.Copula 2) : Measurable fun (u : ↑unitInterval) => ⟨C.conditionalKernel u, ⋯⟩

theorem Verification.lawKernel_comp_map {f : ↑unitInterval → MeasureTheory.ProbabilityMeasure ↑unitInterval} (hf : Measurable f) : (MeasureTheory.Measure.map f MeasureTheory.volume).bind ⇑lawKernel = MeasureTheory.volume.bind ⇑(lawKernel.comap f hf)

Composition with evaluation commutes with the law of a random probability measure.

theorem Verification.conditionalLaw_mem_uniformBarycenter (C : ProbabilityTheory.Copula 2) : conditionalLaw C ∈ uniformBarycenter