Mixtures of kernels

ProbabilityTheory.Kernel.mixture c κ is the kernel whose row at a is the weighted sum ∑ i, c i • κ i a of the rows of a finite family of kernels: the family averaged over a latent index the target does not see. Its rows are finite when the weights are finite and the members are finite kernels.

Main definitions

• ProbabilityTheory.Kernel.mixture — the weighted sum of a finite family of kernels.

Main results

• ProbabilityTheory.Kernel.mixture_apply', ProbabilityTheory.Kernel.mixture_real — a row at an event, in ℝ≥0∞ and on reals.
• ProbabilityTheory.Kernel.mixture_apply_ne_zero_iff — a row has mass on an event exactly when some positively weighted member does.
• ProbabilityTheory.Kernel.isFiniteKernel_mixture — finiteness under finite weights.

noncomputable def ProbabilityTheory.Kernel.mixture {α : Type u_1} {β : Type u_2} {ι : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype ι] (c : ι → ENNReal) (κ : ι → Kernel α β) : Kernel α β

The mixture of a finite family of kernels by weights c: row a is ∑ i, c i • κ i a.

Equations

• ProbabilityTheory.Kernel.mixture c κ = ProbabilityTheory.Kernel.ofFunOfCountable fun (a : α) => ∑ i : ι, c i • (κ i) a

theorem ProbabilityTheory.Kernel.mixture_apply {α : Type u_1} {β : Type u_2} {ι : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype ι] (c : ι → ENNReal) (κ : ι → Kernel α β) (a : α) : (mixture c κ) a = ∑ i : ι, c i • (κ i) a

theorem ProbabilityTheory.Kernel.mixture_apply' {α : Type u_1} {β : Type u_2} {ι : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype ι] (c : ι → ENNReal) (κ : ι → Kernel α β) (a : α) (s : Set β) : ((mixture c κ) a) s = ∑ i : ι, c i * ((κ i) a) s

A row of a mixture at an event is the weighted sum of the members' masses.

theorem ProbabilityTheory.Kernel.mixture_apply_ne_zero_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype ι] (c : ι → ENNReal) (κ : ι → Kernel α β) (a : α) (s : Set β) : ((mixture c κ) a) s ≠ 0 ↔ ∃ (i : ι), c i ≠ 0 ∧ ((κ i) a) s ≠ 0

A row of a mixture has mass on an event exactly when some positively weighted member does.

theorem ProbabilityTheory.Kernel.mixture_real {α : Type u_1} {β : Type u_2} {ι : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype ι] (c : ι → ENNReal) (κ : ι → Kernel α β) [∀ (i : ι), IsFiniteKernel (κ i)] (hc : ∀ (i : ι), c i ≠ ⊤) (a : α) (s : Set β) : ((mixture c κ) a).real s = ∑ i : ι, (c i).toReal * ((κ i) a).real s

A row of a mixture of finite kernels with finite weights at an event, on reals.

theorem ProbabilityTheory.Kernel.isFiniteKernel_mixture {α : Type u_1} {β : Type u_2} {ι : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype ι] (c : ι → ENNReal) (κ : ι → Kernel α β) [∀ (i : ι), IsFiniteKernel (κ i)] (hc : ∀ (i : ι), c i ≠ ⊤) : IsFiniteKernel (mixture c κ)

A mixture of finite kernels with finite weights is a finite kernel.