An augmented latent kernel

The extra Unit branch records the atom at one. The other branch records a strict below/above pair. Thus a single latent parameter always determines a mean-one law supported on at most two points.

@[reducible, inline]

abbrev Feige.AugmentedTwoPointParams : Type

A latent coordinate is either the distinguished atom at one or a genuine strict two-point parameter.

Equations

• Feige.AugmentedTwoPointParams = (Unit ⊕ Feige.TwoPointParams)

noncomputable def Feige.augmentedTwoPointKernel : ProbabilityTheory.Kernel AugmentedTwoPointParams ℝ

The conditional coordinate kernel attached to an augmented parameter.

Equations

• Feige.augmentedTwoPointKernel = { toFun := Sum.elim (fun (x : Unit) => MeasureTheory.Measure.dirac 1) ⇑Feige.twoPointKernel, measurable' := Feige.augmentedTwoPointKernel._proof_1 }

@[simp]

theorem Feige.augmentedTwoPointKernel_atom : augmentedTwoPointKernel (Sum.inl ()) = MeasureTheory.Measure.dirac 1

@[simp]

theorem Feige.augmentedTwoPointKernel_pair (p : TwoPointParams) : augmentedTwoPointKernel (Sum.inr p) = twoPointMeasure (↑p).1 (↑p).2

instance Feige.instIsMarkovKernelAugmentedTwoPointParamsRealAugmentedTwoPointKernel : ProbabilityTheory.IsMarkovKernel augmentedTwoPointKernel

theorem Feige.augmentedTwoPointKernel_mean (p : AugmentedTwoPointParams) : ∫ (x : ℝ), x ∂augmentedTwoPointKernel p = 1

Every conditional law selected by an augmented parameter has mean one.

theorem Feige.augmentedTwoPointKernel_support (p : AugmentedTwoPointParams) : (augmentedTwoPointKernel p) (match p with | Sum.inl val => {1}ᶜ | Sum.inr q => {(↑q).1, (↑q).2}ᶜ) = 0

Every conditional law is concentrated on either one point or the two points encoded by its latent parameter.

noncomputable def Feige.augmentedLatentMeasure (μ : MeasureTheory.Measure ℝ) (M : ℝ) : MeasureTheory.Measure AugmentedTwoPointParams

The complete latent law: its left branch carries the atom at one, and its right branch carries the nondegenerate parameter measure.

Equations

• Feige.augmentedLatentMeasure μ M = μ {1} • MeasureTheory.Measure.dirac (Sum.inl ()) + MeasureTheory.Measure.map Sum.inr (Feige.latentParamsMeasure μ M)

theorem Feige.augmentedLatentMeasure_apply_atom (μ : MeasureTheory.Measure ℝ) (M : ℝ) : (augmentedLatentMeasure μ M) (Set.range Sum.inl) = μ {1}

theorem Feige.augmentedTwoPointKernel_comp_latent (μ : MeasureTheory.Measure ℝ) (M : ℝ) : (augmentedLatentMeasure μ M).bind ⇑augmentedTwoPointKernel = fullKernelMixture μ M

Binding the augmented latent law against its conditional kernel gives exactly the full one-coordinate mixture.

theorem Feige.augmentedLatentMeasure_isProbability {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) (hmean : ∫ (x : ℝ), x ∂μ = 1) (hM : 0 < belowMoment μ) : MeasureTheory.IsProbabilityMeasure (augmentedLatentMeasure μ (belowMoment μ))

Under the hypotheses of the decomposition, the complete latent law is itself a probability measure.

theorem Feige.lintegral_augmentedTwoPointKernel_comp (μ : MeasureTheory.Measure ℝ) (M : ℝ) (f : ℝ → ENNReal) (hf : Measurable f) : ∫⁻ (x : ℝ), f x ∂fullKernelMixture μ M = ∫⁻ (p : AugmentedTwoPointParams), ∫⁻ (x : ℝ), f x ∂augmentedTwoPointKernel p ∂augmentedLatentMeasure μ M

The bind/Tonelli identity for the complete one-coordinate latent decomposition.