Means and covariances of probability mixtures

A mixture's expectation is the expectation of its component means. Its covariance is the expected component covariance plus the covariance of the component means; taking the same observable twice gives the law of total variance.

The mixing measure is a probability measure and the components need be probability measures only almost everywhere. Finite second moments of the mixture imply the required integrability of component means and covariances. The covariance formula applies to any pair of real observables, including coordinates of a vector-valued law.

The integration steps use Mathlib's kernel-composition theory through TauCeti.MeasureTheory.Integral.Bind.

theorem TauCeti.Probability.memLp_integral_bind {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {K : α → MeasureTheory.Measure β} {X : β → ℝ} (hK : Measurable K) (hprob : ∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (K a)) (hX : MeasureTheory.MemLp X 2 (μ.bind K)) : MeasureTheory.MemLp (fun (a : α) => ∫ (x : β), X x ∂K a) 2 μ

Component means of a square-integrable real observable are square-integrable under the mixing law, even when the components are probability measures only almost everywhere.

theorem TauCeti.Probability.integrable_covariance_bind {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {K : α → MeasureTheory.Measure β} {X Y : β → ℝ} (hK : Measurable K) (hprob : ∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (K a)) (hX : MeasureTheory.MemLp X 2 (μ.bind K)) (hY : MeasureTheory.MemLp Y 2 (μ.bind K)) : MeasureTheory.Integrable (fun (a : α) => ProbabilityTheory.covariance X Y (K a)) μ

The component covariances of two square-integrable observables are integrable under the mixing law.

theorem TauCeti.Probability.covariance_bind {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {K : α → MeasureTheory.Measure β} {X Y : β → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hK : Measurable K) (hprob : ∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (K a)) (hX : MeasureTheory.MemLp X 2 (μ.bind K)) (hY : MeasureTheory.MemLp Y 2 (μ.bind K)) : ProbabilityTheory.covariance X Y (μ.bind K) = ∫ (a : α), ProbabilityTheory.covariance X Y (K a) ∂μ + ProbabilityTheory.covariance (fun (a : α) => ∫ (x : β), X x ∂K a) (fun (a : α) => ∫ (x : β), Y x ∂K a) μ

Law of total covariance: a probability mixture's covariance is the sum of the expected component covariance and the covariance of component means.

theorem TauCeti.Probability.variance_bind {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {K : α → MeasureTheory.Measure β} {X : β → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hK : Measurable K) (hprob : ∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (K a)) (hX : MeasureTheory.MemLp X 2 (μ.bind K)) : ProbabilityTheory.variance X (μ.bind K) = ∫ (a : α), ProbabilityTheory.variance X (K a) ∂μ + ProbabilityTheory.variance (fun (a : α) => ∫ (x : β), X x ∂K a) μ

Law of total variance: a probability mixture's variance is its expected component variance plus the variance of the component means.

theorem TauCeti.Probability.evariance_prod_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {π : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure π] {F : α × β → ℝ} (hL : MeasureTheory.MemLp F 2 (μ.prod π)) : ProbabilityTheory.evariance F (μ.prod π) = ∫⁻ (a : α), ProbabilityTheory.evariance (fun (w : β) => F (a, w)) π ∂μ + ProbabilityTheory.evariance (fun (a : α) => ∫ (w : β), F (a, w) ∂π) μ

The law of total variance on a product of probability spaces: the variance of a square integrable F splits into the average of the variances in the second coordinate and the variance of the average over the second coordinate.

theorem ProbabilityTheory.Kernel.covariance_comp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {X Y : β → ℝ} (κ : Kernel α β) [IsMarkovKernel κ] (hX : MeasureTheory.MemLp X 2 (μ.bind ⇑κ)) (hY : MeasureTheory.MemLp Y 2 (μ.bind ⇑κ)) : covariance X Y (μ.bind ⇑κ) = ∫ (a : α), covariance X Y (κ a) ∂μ + covariance (fun (a : α) => ∫ (x : β), X x ∂κ a) (fun (a : α) => ∫ (x : β), Y x ∂κ a) μ

The law of total covariance for the composition of a probability measure and a Markov kernel.

theorem ProbabilityTheory.Kernel.variance_comp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {X : β → ℝ} (κ : Kernel α β) [IsMarkovKernel κ] (hX : MeasureTheory.MemLp X 2 (μ.bind ⇑κ)) : variance X (μ.bind ⇑κ) = ∫ (a : α), variance X (κ a) ∂μ + variance (fun (a : α) => ∫ (x : β), X x ∂κ a) μ

The law of total variance for the composition of a probability measure and a Markov kernel.