InformationTheory.Probability.Mixture

Imports 5

Mixing two measures at a clamped weight #

A probability measure is smoothed toward a second one by taking their convex combination. Clamping the weight to [0, 1] makes the combination a probability measure for every real weight, so the instance is available before any side condition on the weight is discharged, and the mixture may be formed and reasoned about for an unconstrained parameter. On a singleton the mixture is the convex combination of the two masses, so it is positive as soon as the weight is and the second measure charges that point, and it depends continuously on the weight.

Main definitions #

mixWeight ε — the weight ε clamped to [0, 1].
mixLaw p μ₀ ε — the convex combination of p and μ₀ at the clamped weight ε.

Main statements #

mixLaw_real_apply — the singleton mass of the mixture is the convex combination of the two singleton masses.
mixLaw_real_pos — at a positive weight the mixture charges every point the second measure charges.
mixLaw_real_continuous — a singleton mass of the mixture depends continuously on the weight.

Implementation notes #

The module sits at the bottom of the import DAG — it depends only on Mathlib — so any file forming such a mixture can import it without pulling in information-theoretic material.

The clamped weight #

noncomputable def

InformationTheory.mixWeight

source

(ε : ℝ) :

ℝ

The weight ε clamped to [0, 1], so that a convex combination taken at it is a probability measure for every real ε while the weight agrees with ε on [0, 1].

Equations

InformationTheory.mixWeight ε = min 1 (max 0 ε)

Instances For

Used by

theorem

InformationTheory.mixWeight_nonneg

source

(ε : ℝ) :

0 ≤ mixWeight ε

Used by

theorem

InformationTheory.mixWeight_le_one

source

(ε : ℝ) :

mixWeight ε ≤ 1

Used by

theorem

InformationTheory.mixWeight_zero

source

mixWeight 0 = 0

Used by

theorem

InformationTheory.mixWeight_pos

source

{ε : ℝ} (hε : 0 < ε) :

0 < mixWeight ε

Used by

theorem

InformationTheory.mixWeight_continuous

source

Continuous mixWeight

Used by

The mixture #

noncomputable def

InformationTheory.mixLaw

source

{X : Type u_1} [MeasurableSpace X] (p μ₀ : MeasureTheory.Measure X) (ε : ℝ) :

MeasureTheory.Measure X

The convex combination mixLaw p μ₀ ε = (1 - mixWeight ε) • p + mixWeight ε • μ₀ of two measures at the clamped weight ε. For 0 < ε and a μ₀ charging every point, so does the mixture; at ε = 0 it is p.

Equations