The convex structure on exchangeable path laws

Exchangeable probability laws on ℕ → α are closed under convex combination (ExchangeableLaw.smul_add_smul), so the subtype they form carries the convex structure of ProbabilityMeasure. This file names that combination.

It is generic path-law API: nothing here mentions the de Finetti representation. Keeping it out of DeFinetti/Correspondence.lean is what lets a client use the convex structure without depending on the correspondence theory, even though the affinity of deFinettiEquiv is what it was built for.

Main results

• ExchangeableLaw.smul_add_smul — the unbundled closure of exchangeability under nonnegative linear combination, the prerequisite for the bundling.
• exchangeableLawConvexComb — the combination, with toMeasure_exchangeableLawConvexComb exposing its underlying measure.

theorem TauCeti.Probability.ExchangeableLaw.smul_add_smul {α : Type u_1} [MeasurableSpace α] {ρ₁ ρ₂ : MeasureTheory.Measure (ℕ → α)} (h₁ : ExchangeableLaw ρ₁) (h₂ : ExchangeableLaw ρ₂) (a b : ENNReal) : ExchangeableLaw (a • ρ₁ + b • ρ₂)

Exchangeable laws are closed under convex combination, and more generally under any nonnegative linear combination: the defining invariance is an equation between pushforwards, and Measure.map along the (measurable) reindexing is additive and homogeneous.

noncomputable def TauCeti.Probability.exchangeableLawConvexComb {α : Type u_1} [MeasurableSpace α] {a b : ENNReal} (hab : a + b = 1) (ρ₁ ρ₂ : { ρ : MeasureTheory.ProbabilityMeasure (ℕ → α) // ExchangeableLaw ↑ρ }) : { ρ : MeasureTheory.ProbabilityMeasure (ℕ → α) // ExchangeableLaw ↑ρ }

The convex combination of two exchangeable path laws, in the subtype of exchangeable probability measures on ℕ → α. Exchangeability is preserved because the defining permutation invariance is linear (ExchangeableLaw.smul_add_smul).

Equations

• TauCeti.Probability.exchangeableLawConvexComb hab ρ₁ ρ₂ = ⟨MeasureTheory.ProbabilityMeasure.convexComb hab ↑ρ₁ ↑ρ₂, ⋯⟩

@[simp]

theorem TauCeti.Probability.toMeasure_exchangeableLawConvexComb {α : Type u_1} [MeasurableSpace α] {a b : ENNReal} (hab : a + b = 1) (ρ₁ ρ₂ : { ρ : MeasureTheory.ProbabilityMeasure (ℕ → α) // ExchangeableLaw ↑ρ }) : ↑↑(exchangeableLawConvexComb hab ρ₁ ρ₂) = a • ↑↑ρ₁ + b • ↑↑ρ₂

The underlying measure of a convex combination of exchangeable laws.