A total augmented mixture for mean-one laws

The positive-moment branch uses the latent two-point measure from Lemma 4.6. When the lower moment vanishes, the original law is δ₁, so the latent law is simply the atom branch. This removes the artificial coordinatewise strict-moment assumption from the finite product mixture.

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

The augmented latent law, including the degenerate zero-below-moment case.

Equations

• Feige.meanOneAugmentedLatent μ = if Feige.belowMoment μ = 0 then MeasureTheory.Measure.dirac (Sum.inl ()) else Feige.augmentedLatentMeasure μ (Feige.belowMoment μ)

theorem Feige.meanOneAugmentedLatent_isProbability {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) (hmean : ∫ (x : ℝ), x ∂μ = 1) : MeasureTheory.IsProbabilityMeasure (meanOneAugmentedLatent μ)

theorem Feige.augmentedTwoPointKernel_comp_meanOneLatent {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) (hmean : ∫ (x : ℝ), x ∂μ = 1) : (meanOneAugmentedLatent μ).bind ⇑augmentedTwoPointKernel = μ

theorem Feige.pi_eq_recursiveMeanOneAugmented_mixture (n : ℕ) (μ : Fin n → MeasureTheory.Measure ℝ) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (hμ : ∀ (i : Fin n), MeasureTheory.Integrable (fun (x : ℝ) => x) (μ i)) (hmean : ∀ (i : Fin n), ∫ (x : ℝ), x ∂μ i = 1) : (recursiveAugmentedLatent n fun (i : Fin n) => meanOneAugmentedLatent (μ i)).bind ⇑(recursiveAugmentedKernel n) = MeasureTheory.Measure.pi μ

Every finite product of mean-one laws is a mixture of the conditionally independent augmented two-point systems, including all degenerate δ₁ coordinates.