Probability mixtures

This file supplies distribution-level formulas for mixtures of measurable families of measures. Cumulative distribution functions, moment-generating functions, and characteristic functions are the corresponding integrals of the component quantities under their natural hypotheses. It also connects a jointly measurable family of component densities to HasPDF.

The density results allow the component presentation to hold only almost everywhere for the mixing measure. This is useful for kernels whose values away from the valid parameter set are an arbitrary measurable extension.

Main results

• MeasureTheory.Measure.cdf_bind computes the cdf of a real-valued probability mixture whose components are probability measures almost everywhere.
• MeasureTheory.Measure.mem_integrableExpSet_bind_iff characterizes the exact exponential integrability domain by an iterated nonnegative integral.
• MeasureTheory.Measure.mgf_bind, MeasureTheory.Measure.cgf_bind, and MeasureTheory.Measure.charFun_bind express transforms of mixtures in terms of their components.
• TauCeti.Probability.hasPDF_of_hasLaw_bind_withDensity gives the density interface for a random variable whose law is a mixture of densities.

theorem MeasureTheory.Measure.cdf_bind {A : Type u_1} [MeasurableSpace A] (rho : Measure A) [IsProbabilityMeasure rho] (K : A → Measure ℝ) (hK : AEMeasurable K rho) (hprob : ∀ᵐ (a : A) ∂rho, IsProbabilityMeasure (K a)) (x : ℝ) : ↑(ProbabilityTheory.cdf (rho.bind K)) x = ∫ (a : A), ↑(ProbabilityTheory.cdf (K a)) x ∂rho

The cdf of a mixture of real probability laws is the integral of their cdfs.

theorem MeasureTheory.Measure.mem_integrableExpSet_bind_iff {A : Type u_1} [MeasurableSpace A] {B : Type u_2} [MeasurableSpace B] (rho : Measure A) {K : A → Measure B} (hK : AEMeasurable K rho) {X : B → ℝ} (hX : Measurable X) (t : ℝ) : t ∈ ProbabilityTheory.integrableExpSet X (rho.bind K) ↔ ∫⁻ (a : A), ∫⁻ (x : B), ENNReal.ofReal (Real.exp (t * X x)) ∂K a ∂rho < ⊤

Exponential integrability under a mixture is equivalent to finiteness of the iterated nonnegative exponential integral. This formulation remains meaningful before passing to real mgfs and records the exact integrability domain without relying on totalized real integration.

theorem MeasureTheory.Measure.mgf_bind {A : Type u_1} [MeasurableSpace A] {B : Type u_2} [MeasurableSpace B] (rho : Measure A) {K : A → Measure B} (hK : AEMeasurable K rho) (X : B → ℝ) (t : ℝ) (ht : t ∈ ProbabilityTheory.integrableExpSet X (rho.bind K)) : ProbabilityTheory.mgf X (rho.bind K) t = ∫ (a : A), ProbabilityTheory.mgf X (K a) t ∂rho

On its integrability domain, the mgf of a mixture is the integral of the component mgfs.

theorem MeasureTheory.Measure.cgf_bind {A : Type u_1} [MeasurableSpace A] {B : Type u_2} [MeasurableSpace B] (rho : Measure A) {K : A → Measure B} (hK : AEMeasurable K rho) (X : B → ℝ) (t : ℝ) (ht : t ∈ ProbabilityTheory.integrableExpSet X (rho.bind K)) : ProbabilityTheory.cgf X (rho.bind K) t = Real.log (∫ (a : A), ProbabilityTheory.mgf X (K a) t ∂rho)

The cgf of a mixture is the logarithm of the integral of the component mgfs, rather than the integral of their cgfs.

theorem MeasureTheory.Measure.charFun_bind {A : Type u_1} [MeasurableSpace A] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (rho : Measure A) {K : A → Measure E} (hK : AEMeasurable K rho) [IsFiniteMeasure (rho.bind K)] (t : E) : charFun (rho.bind K) t = ∫ (a : A), charFun (K a) t ∂rho

The characteristic function of a mixture of finite total mass is the integral of the component characteristic functions.

noncomputable def TauCeti.Probability.finiteMixtureMeasure {I : Type u_1} [Fintype I] {B : Type u_3} [MeasurableSpace B] (p : Convexity.StdSimplex NNReal I) (K : I → MeasureTheory.Measure B) : MeasureTheory.Measure B

The finite mixture of a family of measures with simplex weights.

theorem TauCeti.Probability.finiteMixtureMeasure_def {I : Type u_1} [Fintype I] {B : Type u_3} [MeasurableSpace B] (p : Convexity.StdSimplex NNReal I) (K : I → MeasureTheory.Measure B) : finiteMixtureMeasure p K = ∑ i : I, ↑(p.weights i) • K i

A finite mixture is its defining weighted sum.

instance TauCeti.Probability.isProbabilityMeasure_finiteMixtureMeasure {I : Type u_1} [Fintype I] {B : Type u_3} [MeasurableSpace B] {p : Convexity.StdSimplex NNReal I} {K : I → MeasureTheory.Measure B} [hK : ∀ (i : I), MeasureTheory.IsProbabilityMeasure (K i)] : MeasureTheory.IsProbabilityMeasure (finiteMixtureMeasure p K)

A finite mixture of probability measures is a probability measure.

@[simp]

theorem TauCeti.Probability.toFiniteMeasure_finiteMixtureMeasure {I : Type u_1} [Fintype I] {B : Type u_3} [MeasurableSpace B] (p : Convexity.StdSimplex NNReal I) (K : I → MeasureTheory.ProbabilityMeasure B) : (finiteMixtureMeasure p fun (i : I) => ↑(K i)).toProbabilityMeasure.toFiniteMeasure = ∑ i : I, p.weights i • (K i).toFiniteMeasure

Viewed as a finite measure, a probability mixture is the weighted sum of the finite measures associated to its components.

theorem TauCeti.Probability.finiteMixtureMeasure_eq_bind {I : Type u_1} [Fintype I] {B : Type u_3} [MeasurableSpace B] [MeasurableSpace I] [MeasurableSingletonClass I] (p : Convexity.StdSimplex NNReal I) (K : I → MeasureTheory.Measure B) : finiteMixtureMeasure p K = (categoricalMeasure p).bind K

A finite mixture is the categorical mixture of its components.

@[simp]

theorem TauCeti.Probability.finiteMixtureMeasure_const {I : Type u_1} [Fintype I] {B : Type u_3} [MeasurableSpace B] (p : Convexity.StdSimplex NNReal I) (mu : MeasureTheory.Measure B) : (finiteMixtureMeasure p fun (x : I) => mu) = mu

A finite mixture of identical components is that component.

theorem TauCeti.Probability.finiteMixtureMeasure_congr {I : Type u_1} [Fintype I] {B : Type u_3} [MeasurableSpace B] {p : Convexity.StdSimplex NNReal I} {K L : I → MeasureTheory.Measure B} (h : ∀ (i : I), 0 < p.weights i → K i = L i) : finiteMixtureMeasure p K = finiteMixtureMeasure p L

Changing zero-weight components leaves a finite mixture unchanged.

theorem TauCeti.Probability.measurable_finiteMixtureMeasure {I : Type u_1} {Z : Type u_2} [Fintype I] {B : Type u_3} [MeasurableSpace B] [MeasurableSpace Z] {p : Z → Convexity.StdSimplex NNReal I} {K : Z → I → MeasureTheory.Measure B} (hp : Measurable p) (hK : ∀ (i : I), Measurable fun (z : Z) => K z i) : Measurable fun (z : Z) => finiteMixtureMeasure (p z) (K z)

Finite mixtures are measurable when their weights and components are measurable.

theorem TauCeti.Probability.integrable_finiteMixtureMeasure_iff {I : Type u_1} [Fintype I] {B : Type u_3} [MeasurableSpace B] {p : Convexity.StdSimplex NNReal I} {K : I → MeasureTheory.Measure B} {E : Type u_4} [NormedAddCommGroup E] {f : B → E} : MeasureTheory.Integrable f (finiteMixtureMeasure p K) ↔ ∀ (i : I), 0 < p.weights i → MeasureTheory.Integrable f (K i)

Integrability under a finite mixture is integrability under every positive-weight component.

theorem TauCeti.Probability.integral_finiteMixtureMeasure {I : Type u_1} [Fintype I] {B : Type u_3} [MeasurableSpace B] {p : Convexity.StdSimplex NNReal I} {K : I → MeasureTheory.Measure B} {E : Type u_4} [NormedAddCommGroup E] {f : B → E} [NormedSpace ℝ E] (hf : MeasureTheory.Integrable f (finiteMixtureMeasure p K)) : ∫ (x : B), f x ∂finiteMixtureMeasure p K = ∑ i : I, ↑(p.weights i) • ∫ (x : B), f x ∂K i

The integral under a finite mixture is the weighted sum of the component integrals.

theorem TauCeti.Probability.memLp_finiteMixtureMeasure {I : Type u_1} [Fintype I] {B : Type u_3} [MeasurableSpace B] {p : Convexity.StdSimplex NNReal I} {K : I → MeasureTheory.Measure B} {E : Type u_4} [NormedAddCommGroup E] {f : B → E} {q : ENNReal} (hf : ∀ (i : I), 0 < p.weights i → MeasureTheory.MemLp f q (K i)) : MeasureTheory.MemLp f q (finiteMixtureMeasure p K)

A finite mixture has an Lᵖ observable when every positive-weight component does.

theorem TauCeti.Probability.hasPDF_of_hasLaw_bind_withDensity {Omega : Type u_1} {A : Type u_2} {B : Type u_3} [MeasurableSpace Omega] [MeasurableSpace A] [MeasurableSpace B] {P : MeasureTheory.Measure Omega} {rho : MeasureTheory.Measure A} {nu : MeasureTheory.Measure B} {K : A → MeasureTheory.Measure B} {f : A → B → ENNReal} {X : Omega → B} [MeasureTheory.SFinite rho] [MeasureTheory.SFinite nu] (hf : Measurable (Function.uncurry f)) (hKf : K =ᵐ[rho] fun (a : A) => nu.withDensity (f a)) (hX : ProbabilityTheory.HasLaw X (rho.bind K) P) : MeasureTheory.HasPDF X P nu

A random variable whose law is a mixture of jointly measurable component densities has the integrated component density.

theorem TauCeti.Probability.pdf_eq_of_hasLaw_bind_withDensity {Omega : Type u_1} {A : Type u_2} {B : Type u_3} [MeasurableSpace Omega] [MeasurableSpace A] [MeasurableSpace B] {P : MeasureTheory.Measure Omega} {rho : MeasureTheory.Measure A} {nu : MeasureTheory.Measure B} {K : A → MeasureTheory.Measure B} {f : A → B → ENNReal} {X : Omega → B} [MeasureTheory.SFinite rho] [MeasureTheory.SigmaFinite nu] (hf : Measurable (Function.uncurry f)) (hKf : K =ᵐ[rho] fun (a : A) => nu.withDensity (f a)) (hX : ProbabilityTheory.HasLaw X (rho.bind K) P) : MeasureTheory.pdf X P nu =ᵐ[nu] fun (b : B) => ∫⁻ (a : A), f a b ∂rho

The pdf selected by Mathlib for a mixture of component densities agrees almost everywhere with their pointwise integral.