A fixed normalized finite mixture preserves a common invariant measure

AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixture.finiteMixture_invariant · theorem · Teaching coverage

Statement

Let I be a finite index type and A an arbitrary measurable space. Let Kᵢ:A→𝓜(A) be s-finite kernels, and let μ be any measure on A. Suppose each component preserves the same μ. If the fixed nonnegative real weights wᵢ sum to one, then their finite mixture M_w also preserves μ. The component kernels need not be Markov, and the target μ need not be finite, s-finite, nonzero or normalized.

All objects and hypotheses

• Implicit parameters actually used by this declaration: {ι α : Type*}, [Fintype ι], [MeasurableSpace α]. The preceding section also declares β and its measurable structure, but they are unused here and are not parameters of this result.
• w : ι → ℝ≥0, fixed independently of the input state.
• κ : ι → Kernel α α with [∀ i, IsSFiniteKernel (κ i)].
• μ : Measure α, completely arbitrary as a measure.
• hsum : ∑ i, w i = 1.
• hκ : ∀ i, (κ i).Invariant μ, meaning μ.bind (κ i)=μ for every i.
• No Markov, finite-target, s-finite-target, probability-target, domination or Bochner integrability hypothesis.

Notation and interpretation

Measurable space and kernel

A measurable space is a set with a specified sigma-algebra of events. A kernel K from A to B assigns to each input a a measure K(a,·) on B, and a↦K(a,E) is measurable whenever E is measurable. A kernel need not assign probability measures unless Markovness is separately assumed.

\[K:A\to\mathcal M(B),\qquad a\mapsto K(a,E)\text{ measurable for every measurable }E\subseteq B.\]

Measure evolved by a kernel; invariance

Write μK for the measure obtained by starting with μ and applying K. Lean writes μ.bind K or K ∘ₘ μ. Invariance says that this evolved measure is exactly μ. If μ is a probability law this means a stationary initial distribution, but the definitions and these theorems also allow arbitrary measures.

\[(\mu K)(E)=\int_A K(a,E)\,\mu(da),\qquad \mu K=\mu.\]

Composition and powers

Lean's L ∘ₖ K applies K first and L second. The multiplicative identity is the identity kernel a↦δ_a, and powers are repeated composition. All integrals here are nonnegative extended-real (lower Lebesgue) integrals; no signed or Bochner integrability is silently assumed.

\[(L\circ_{\!k}K)(a,E)=\int L(b,E)\,K(a,db),\quad K^0(a,\cdot)=\delta_a,\quad K^{n+1}=K^n\circ_{\!k}K.\]

Markov and s-finite kernels

Markov means every output measure has total mass one. An s-finite kernel is a countable sum of finite kernels, where each finite kernel has a finite uniform bound on its total mass across inputs. Markovness supplies this s-finiteness automatically. S-finite is not the same hypothesis as sigma-finite, and is not merely a pointwise finiteness assertion.

\[K(a,B)=1\ \forall a\quad\text{(Markov)};\qquad K=\sum_{n=0}^{\infty}K_n,\quad \forall n\ \exists C_n<\infty\ \forall a,\ K_n(a,B)\le C_n\quad\text{(s-finite)}.\]

Nonnegative weights

ℝ≥0 consists of finite nonnegative real numbers; ℝ≥0∞ also allows infinity and is the codomain of measure values. The coercion wᵢ↦cᵢ puts finite weights into extended nonnegative arithmetic. Zero weights are permitted, including when component masses are infinite; this arithmetic uses 0·∞=0.

\[w_i\in[0,\infty),\qquad c_i=\iota(w_i)\in[0,\infty].\]

Measurable equivalence and pushforward

A measurable equivalence e is a bijection whose forward and inverse maps are both measurable. Its pushforward measure records the original mass of inverse images. This is transport of measures, not a density transformation with an implicit Jacobian.

\[(e_*\mu)(E)=\mu(e^{-1}(E)),\qquad (e^{-1})_*(e_*\mu)=\mu.\]

Mathematical proof

have hsum' : ∑ i, (w i : ℝ≥0∞) = 1 := by
  simpa using congrArg (fun r : ℝ≥0 => (r : ℝ≥0∞)) hsum

change μ.bind (finiteMixture w κ) = μ
ext s hs
calc
  (μ.bind (finiteMixture w κ)) s = ∫⁻ a, ∑ i, (w i : ℝ≥0∞) * κ i a s ∂μ := by
    rw [Measure.bind_apply hs (Kernel.aemeasurable _)]
    simp only [finiteMixture_apply, Measure.finsetSum_apply, Measure.smul_apply, smul_eq_mul]

_ = ∑ i, ∫⁻ a, (w i : ℝ≥0∞) * κ i a s ∂μ :=
  lintegral_finsetSum _ (fun i _ => ((κ i).measurable_coe hs).const_mul _)

_ = ∑ i, (w i : ℝ≥0∞) * μ s := by
  apply Finset.sum_congr rfl
  intro i _
  rw [lintegral_const_mul _ ((κ i).measurable_coe hs),
    ← Measure.bind_apply hs (κ i).aemeasurable, (hκ i).def]

theorem finiteMixture_invariant (w : ι → ℝ≥0) (κ : ι → Kernel α α)
    [∀ i, IsSFiniteKernel (κ i)] (μ : Measure α)
    (hsum : ∑ i, w i = 1) (hκ : ∀ i, (κ i).Invariant μ) :
    (finiteMixture w κ).Invariant μ

theorem finiteMixture_invariant (w : ι → ℝ≥0) (κ : ι → Kernel α α)
    [∀ i, IsSFiniteKernel (κ i)] (μ : Measure α)
    (hsum : ∑ i, w i = 1) (hκ : ∀ i, (κ i).Invariant μ) :
    (finiteMixture w κ).Invariant μ := by
  have hsum' : ∑ i, (w i : ℝ≥0∞) = 1 := by
    simpa using congrArg (fun r : ℝ≥0 => (r : ℝ≥0∞)) hsum
  change μ.bind (finiteMixture w κ) = μ
  ext s hs
  calc
    (μ.bind (finiteMixture w κ)) s = ∫⁻ a, ∑ i, (w i : ℝ≥0∞) * κ i a s ∂μ := by
      rw [Measure.bind_apply hs (Kernel.aemeasurable _)]
      simp only [finiteMixture_apply, Measure.finsetSum_apply, Measure.smul_apply, smul_eq_mul]
    _ = ∑ i, ∫⁻ a, (w i : ℝ≥0∞) * κ i a s ∂μ :=
      lintegral_finsetSum _ (fun i _ => ((κ i).measurable_coe hs).const_mul _)
    _ = ∑ i, (w i : ℝ≥0∞) * μ s := by
      apply Finset.sum_congr rfl
      intro i _
      rw [lintegral_const_mul _ ((κ i).measurable_coe hs),
        ← Measure.bind_apply hs (κ i).aemeasurable, (hκ i).def]
    _ = μ s := by rw [← Finset.sum_mul, hsum', one_mul]

end AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixture

Scope and omitted-condition boundaries

• No finite or s-finite assumption on μ; do not add one in the reader.
• Only fixed state-independent finite weights. A state-dependent rule cannot use the constant-factor step without a different argument.
• Does not prove reversibility, positive holding probability, aperiodicity, mixing, concrete Gibbs support/normalization, or a sampling implementation.
• HeatBath and KernelInvariance are dependencies of concrete tests/consumers, not proof prerequisites of this generic theorem.
• The theorem as written asks invariance of every component, even if its weight is zero; it does not export a weaker positive-weight-only hypothesis.
• Source-neutral interface; no numbered source theorem or source-copy-index repair is claimed.