Coordinatewise two-point mixtures

This file lifts the one-dimensional measurable two-point decomposition to a finite independent product. It is the product-measure interface used in the proof of Theorem 2.1 before conditioning on all latent pairs.

noncomputable def Feige.augmentedConditionalProduct {n : ℕ} (p : Fin n → AugmentedTwoPointParams) : MeasureTheory.Measure (Fin n → ℝ)

Given all latent coordinates, the observations are conditionally independent with the augmented two-point conditional marginals.

Equations

• Feige.augmentedConditionalProduct p = MeasureTheory.Measure.pi fun (i : Fin n) => Feige.augmentedTwoPointKernel (p i)

instance Feige.instIsProbabilityMeasureForallFinRealAugmentedConditionalProduct {n : ℕ} (p : Fin n → AugmentedTwoPointParams) : MeasureTheory.IsProbabilityMeasure (augmentedConditionalProduct p)

theorem Feige.augmentedConditionalProduct_coordinate_mean {n : ℕ} (p : Fin n → AugmentedTwoPointParams) (i : Fin n) : ∫ (x : ℝ), x ∂augmentedTwoPointKernel (p i) = 1

Each coordinate of every conditional product is a mean-one law.

theorem Feige.augmentedConditionalProduct_coordinate_support {n : ℕ} (p : Fin n → AugmentedTwoPointParams) (i : Fin n) : (augmentedTwoPointKernel (p i)) (match p i with | Sum.inl val => {1}ᶜ | Sum.inr q => {(↑q).1, (↑q).2}ᶜ) = 0

Each coordinate of every conditional product is supported on at most two points (one point on the atom branch).

theorem Feige.parallelComp_comp_prod_measure {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel γ δ) [ProbabilityTheory.IsSFiniteKernel η] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure γ) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] : (μ.prod ν).bind ⇑(κ.parallelComp η) = (μ.bind ⇑κ).prod (ν.bind ⇑η)

Binary Fubini exchange: independently binding two latent laws against their coordinate kernels is the same as binding their product against the parallel product kernel. This is the recursion step needed for a finite product.

noncomputable def Feige.finHeadTailEquiv (α : Type u_1) [MeasurableSpace α] (n : ℕ) : (Fin (n + 1) → α) ≃ᵐ α × (Fin n → α)

Measurable head/tail splitting of a homogeneous Fin (n+1) vector.

Equations

• Feige.finHeadTailEquiv α n = MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) => α) 0

noncomputable def Feige.recursiveAugmentedKernel (n : ℕ) : ProbabilityTheory.Kernel (Fin n → AugmentedTwoPointParams) (Fin n → ℝ)

A genuinely measurable finite parallel product of the augmented coordinate kernels. This avoids the unavailable Kernel.pi: the successor case splits head and tail, uses parallelComp, and maps the output pair back to a Fin (n+1) vector.

Equations

• One or more equations did not get rendered due to their size.
• Feige.recursiveAugmentedKernel 0 = ProbabilityTheory.Kernel.const (Fin 0 → Feige.AugmentedTwoPointParams) (MeasureTheory.Measure.dirac fun (i : Fin 0) => i.elim0)

instance Feige.recursiveAugmentedKernel_markov (n : ℕ) : ProbabilityTheory.IsMarkovKernel (recursiveAugmentedKernel n)

theorem Feige.bind_congr_measurableEquiv {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} [MeasurableSpace α] [MeasurableSpace α'] [MeasurableSpace β] [MeasurableSpace β'] (κ : ProbabilityTheory.Kernel α β) (μ : MeasureTheory.Measure α) (eα : α' ≃ᵐ α) (eβ : β' ≃ᵐ β) : (MeasureTheory.Measure.map (⇑eα.symm) μ).bind ⇑((κ.comap ⇑eα ⋯).map ⇑eβ.symm) = MeasureTheory.Measure.map (⇑eβ.symm) (μ.bind ⇑κ)

Binding is invariant under simultaneous measurable-equivalence changes of latent and observation coordinates.

noncomputable def Feige.recursiveAugmentedLatent (n : ℕ) : (Fin n → MeasureTheory.Measure AugmentedTwoPointParams) → MeasureTheory.Measure (Fin n → AugmentedTwoPointParams)

Recursive latent product aligned definitionally with recursiveAugmentedKernel.

Equations

• One or more equations did not get rendered due to their size.
• Feige.recursiveAugmentedLatent 0 = fun (x : Fin 0 → MeasureTheory.Measure Feige.AugmentedTwoPointParams) => MeasureTheory.Measure.dirac fun (i : Fin 0) => i.elim0

noncomputable def Feige.recursiveRealProduct (n : ℕ) : (Fin n → MeasureTheory.Measure ℝ) → MeasureTheory.Measure (Fin n → ℝ)

The analogous head/tail recursive product of observation marginals.

Equations

• One or more equations did not get rendered due to their size.
• Feige.recursiveRealProduct 0 = fun (x : Fin 0 → MeasureTheory.Measure ℝ) => MeasureTheory.Measure.dirac fun (i : Fin 0) => i.elim0

instance Feige.recursiveAugmentedLatent_sfinite (n : ℕ) (latent : Fin n → MeasureTheory.Measure AugmentedTwoPointParams) [∀ (i : Fin n), MeasureTheory.SFinite (latent i)] : MeasureTheory.SFinite (recursiveAugmentedLatent n latent)

theorem Feige.recursiveAugmentedKernel_comp_latent (n : ℕ) (latent : Fin n → MeasureTheory.Measure AugmentedTwoPointParams) [∀ (i : Fin n), MeasureTheory.SFinite (latent i)] : (recursiveAugmentedLatent n latent).bind ⇑(recursiveAugmentedKernel n) = recursiveRealProduct n fun (i : Fin n) => (latent i).bind ⇑augmentedTwoPointKernel

Finite recursive product-of-binds theorem. This is the full induction: the binary Fubini step handles head/tail and the measurable-equivalence conjugation returns to Fin (n+1) coordinates.

theorem Feige.recursiveRealProduct_zero (μ : Fin 0 → MeasureTheory.Measure ℝ) : recursiveRealProduct 0 μ = MeasureTheory.Measure.dirac fun (i : Fin 0) => i.elim0

Zero-dimensional recursive product.

theorem Feige.recursiveRealProduct_eq_pi (n : ℕ) (μ : Fin n → MeasureTheory.Measure ℝ) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] : recursiveRealProduct n μ = MeasureTheory.Measure.pi μ

The head/tail recursive product is the standard finite Measure.pi.