KernelMixture: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Constructing a finite fixed-weight mixture of kernels
The mixture at each input is the weighted sum of output measures
A normalized mixture of Markov kernels is a Markov kernel
A fixed normalized finite mixture preserves a common invariant measure

ASTIS mathematical exposition

Constructing a finite fixed-weight mixture of kernels

AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixture.finiteMixture · def · Teaching coverage

Statement

Let I be a finite index type, A and B measurable spaces, w:I→[0,∞) fixed nonnegative real weights, and Kᵢ kernels from A to B. Assume every Kᵢ is an s-finite kernel. The construction first multiplies each output measure of Kᵢ by the constant density wᵢ, then adds these finitely many kernels. Denote the result by M_w. No sum-to-one condition is needed to define it; the next theorem identifies its value at each input as the weighted sum of component measures.

\[M_w:=\sum_{i\in I}K_i.\operatorname{withDensity}\bigl((a,b)\mapsto c_i\bigr),\qquad c_i=\iota(w_i)\in[0,\infty].\]

All objects and hypotheses

Implicit section variables {ι α β : Type*}.
[Fintype ι]: there are finitely many component indices; this does not make α or β a finite state space.
[MeasurableSpace α] and [MeasurableSpace β].
w : ι → ℝ≥0, fixed independently of input and output states.
κ : ι → Kernel α β.
[∀ i, IsSFiniteKernel (κ i)], a uniform-kernel decomposition contract for each component, required by the chosen withDensity API.
No normalization, strict positivity, Markovness, target measure μ, nonempty-space, Standard-Borel or topological assumption.

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.\]

Construction and meaning

1. Embed the weights into the range of measure values

A measure takes extended nonnegative real values. Regard the finite nonnegative real weight wᵢ as the extended value cᵢ. For each i, the proposed density is the constant function (a,b)↦cᵢ, so it is measurable on the product measurable space.

\[c_i=\iota(w_i),\qquad f_i(a,b)=c_i,\qquad f_i\text{ measurable}.\]

Corresponding Lean step

(fun _ _ => (w i : ℝ≥0∞))

measurable_const is used explicitly in finiteMixture_apply to certify the genuine-density branch; the definition itself passes the density to the totalized API.

2. Form one constant-density kernel for each component

For each i, invoke the existing withDensity construction. At a fixed input a, its intended measure is obtained by integrating the constant cᵢ against Kᵢ(a,·). The s-finite component hypothesis guarantees that the imported construction yields a measurable kernel. Because fᵢ is measurable, the API's nonmeasurable zero fallback is not used; the next evaluation theorem proves this explicitly.

\[L_i:=K_i.\operatorname{withDensity}(f_i),\qquad L_i(a,E)=\int_E c_i\,K_i(a,db)=c_iK_i(a,E).\]

Corresponding Lean step

(κ i).withDensity (fun _ _ => (w i : ℝ≥0∞))

The displayed pointwise interpretation is justified by finiteMixture_apply and its Mathlib helpers, not by an additional theorem proof inside this definition.

3. Add the finitely many kernels

Use the additive structure on kernels to take the finite sum of the Lᵢ. Finite sums of measures remain measures, and the existing kernel sum structure preserves the required input measurability. This defines M_w. If I is empty the sum is the zero kernel.

\[M_w=\sum_{i\in I}L_i.\]

Corresponding Lean step

∑ i, (κ i).withDensity (fun _ _ => (w i : ℝ≥0∞))

These are construction steps, not an invariance or normalization proof.

Lean statement · finiteMixture

This declaration returns a kernel, not a proposition. Fintype supplies the finite summation range. Each κ i is a component kernel. The bracketed family of IsSFiniteKernel assumptions lets Lean construct every withDensity component. The two underscores in fun _ _ mean the density ignores both current and next state. noncomputable indicates an abstract mathematical construction, not an executable sampling implementation.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

noncomputable def finiteMixture (w : ι → ℝ≥0) (κ : ι → Kernel α β)
    [∀ i, IsSFiniteKernel (κ i)] : Kernel α β

Exact module and namespace context

Lean construction · finiteMixture

The displayed body is the definition itself. withDensity weights each component by a constant, and ∑ adds the resulting kernels. The statement does not assert that these masses add to one; that is proved separately only when normalized weights and Markov components are supplied.

noncomputable def finiteMixture (w : ι → ℝ≥0) (κ : ι → Kernel α β)
    [∀ i, IsSFiniteKernel (κ i)] : Kernel α β :=
  ∑ i, (κ i).withDensity (fun _ _ => (w i : ℝ≥0∞))

/-- Pointwise measure law of the finite mixture. Constant uncurry densities are
measurable, so the totalized `withDensity` zero fallback is never used. -/

Exact module and namespace context

Scope and omitted-condition boundaries

This definition alone claims neither Markovness nor invariance.
S-finiteness is the selected Mathlib implementation's contract; this is not a claim that every conceivable finite-mixture definition mathematically needs it.
State-dependent weights, signed weights and computational sampling code are not provided.
Empty I yields the zero kernel; the later hypothesis ∑ᵢwᵢ=1 cannot hold for empty I.
Source-neutral construction; no numbered primary textbook theorem is assigned.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ProbabilityTheory.Kernel.withDensity
ProbabilityTheory.IsSFiniteKernel
ProbabilityTheory.Kernel.instAddCommMonoid
Finset.sum

Mathematical sources

ASTIS mixture construction — Directly inspected definition.
Mathlib withDensity construction — Inspected s-finite assumption and measurable/nonmeasurable branches.
Finite-kernel additive structure — Existing sum infrastructure.
Focused tests (consumer evidence) — Tests preserve the arbitrary-target contract; remove a zero-weight Bool component at the measure level; and use a private Bool family consisting of the identity and heatBathSnd. The latter is Markov, invariant, and reusable in invariant_pow. The identity weight may be zero, so the tests do not establish positive holding probability or aperiodicity.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

ASTIS mathematical exposition

The mixture at each input is the weighted sum of output measures

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

Statement

Let I be a finite index type, A and B measurable spaces, w:I→[0,∞) fixed weights, and Kᵢ:A→𝓜(B) s-finite kernels. For every input a∈A, the output measure of finiteMixture w K is exactly the sum of the scaled measures wᵢKᵢ(a,·). Normalization of w is not assumed. This evaluation identity explains the construction rather than asserting a new convergence property.

\[M_w(a,\cdot)=\sum_{i\in I}c_i\,K_i(a,\cdot),\qquad c_i=\iota(w_i).\qquad M_w(a,E)=\sum_{i\in I}c_iK_i(a,E).\]

All objects and hypotheses

{ι α β : Type*}, [Fintype ι], [MeasurableSpace α], [MeasurableSpace β] from the local section.
w : ι → ℝ≥0 and κ : ι → Kernel α β.
[∀ i, IsSFiniteKernel (κ i)].
a : α is an arbitrary input.
No ∑ᵢwᵢ=1 hypothesis, no Markovness, and no target measure. The primary equality is equality of measures, not merely equality of densities on measurable sets.

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

1. Evaluate the finite kernel sum at the input

Expand the mixture definition. Evaluation of a finite sum of kernels at a fixed input distributes over that sum, leaving one constant-density output measure for each i.

\[M_w(a,\cdot)=\sum_{i\in I}\bigl[K_i.\operatorname{withDensity}(f_i)\bigr](a,\cdot),\qquad f_i(x,b)=c_i.\]

Corresponding Lean step

classical
rw [finiteMixture, sum_apply]

This sum_apply is the root fun-like finite-sum evaluation theorem generated in Mathlib/Algebra/BigOperators/Pi.lean, not ProbabilityTheory.Kernel.sum_apply (which concerns a countable Kernel.sum).

2. Use the genuinely measurable constant-density branch

Fix one index i. The function fᵢ on the product is constant, hence measurable. The withDensity evaluation law therefore identifies the output of the kernel construction with the measure Kᵢ(a,·) carrying the constant density cᵢ. This rules out the API's fallback value.

\[\bigl[K_i.\operatorname{withDensity}(f_i)\bigr](a,\cdot)=K_i(a,\cdot).\operatorname{withDensity}(b\mapsto c_i).\]

Corresponding Lean step

apply Finset.sum_congr rfl
intro i _
rw [Kernel.withDensity_apply _ measurable_const, MeasureTheory.withDensity_const]

The first rewrite in the final rw line performs this step.

3. A constant density is scalar multiplication of a measure

Multiplying a measure by the constant density cᵢ gives precisely the scalar multiple cᵢKᵢ(a,·). Substitute this equality in every summand. The resulting equality is exactly the asserted weighted-sum formula.

\[K_i(a,\cdot).\operatorname{withDensity}(c_i)=c_i\,K_i(a,\cdot),\qquad M_w(a,\cdot)=\sum_i c_iK_i(a,\cdot).\]

Corresponding Lean step

rw [Kernel.withDensity_apply _ measurable_const, MeasureTheory.withDensity_const]

The second rewrite in the same source line performs this step. No division by weights is used, so wᵢ=0 is allowed.

Lean statement · finiteMixture_apply

finiteMixture w κ a is a measure on β. On the right, κ i a is the i-th output measure at a, • multiplies a measure by an extended nonnegative scalar, and ∑ sums measures over the finite index type. The cast (w i : ℝ≥0∞) changes the number type, not the mathematical weight.

theorem finiteMixture_apply (w : ι → ℝ≥0) (κ : ι → Kernel α β)
    [∀ i, IsSFiniteKernel (κ i)] (a : α) :
    finiteMixture w κ a = ∑ i, (w i : ℝ≥0∞) • κ i a

Exact module and namespace context

Lean proof · finiteMixture_apply

After distributing evaluation over the finite sum, it suffices to check one summand. measurable_const verifies the joint measurability required by withDensity_apply, and withDensity_const turns constant density into scalar multiplication. classical supplies finite-index bookkeeping without an extra mathematical hypothesis.

theorem finiteMixture_apply (w : ι → ℝ≥0) (κ : ι → Kernel α β)
    [∀ i, IsSFiniteKernel (κ i)] (a : α) :
    finiteMixture w κ a = ∑ i, (w i : ℝ≥0∞) • κ i a := by
  classical
  rw [finiteMixture, sum_apply]
  apply Finset.sum_congr rfl
  intro i _
  rw [Kernel.withDensity_apply _ measurable_const, MeasureTheory.withDensity_const]

/-- Fixed normalized nonnegative weights mix Markov kernels into a Markov kernel.
Zero weights are allowed. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Evaluation interface only: no probability normalization, common target, invariance, reversibility or mixing result.
A finite family of arbitrary state spaces is allowed; no finite-state restriction is introduced.
This proof establishes that constant densities avoid withDensity's nonmeasurable zero branch.
No independently checked primary textbook anchor; exact proof sources are the local definition and Mathlib identities.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixture.finiteMixture

Mathlib API called (external library)

sum_apply
Finset.sum_congr
ProbabilityTheory.Kernel.withDensity_apply
measurable_const
MeasureTheory.withDensity_const

Mathematical sources

ASTIS pointwise measure identity — Directly inspected theorem and proof.
Mathlib kernel density evaluation — Genuine measurable branch.
Mathlib constant-density measure identity — Scalar-multiple identity.
Mathlib root finite-sum evaluation — sum_apply is the additive theorem generated by the to_additive annotation on prod_apply.
Focused tests (consumer evidence) — Tests preserve the arbitrary-target contract; remove a zero-weight Bool component at the measure level; and use a private Bool family consisting of the identity and heatBathSnd. The latter is Markov, invariant, and reusable in invariant_pow. The identity weight may be zero, so the tests do not establish positive holding probability or aperiodicity.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

ASTIS mathematical exposition

A normalized mixture of Markov kernels is a Markov kernel

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

Statement

Let I be a finite index type, A and B measurable spaces, and Kᵢ Markov kernels from A to B. Let wᵢ be fixed nonnegative real weights whose sum is one. Then the finite mixture M_w is a Markov kernel: for every input a, its output measure is a probability measure. Individual weights may be zero.

\[\left[\forall i,a,\ K_i(a,B)=1\right]\ \land\ \left[\sum_{i\in I}w_i=1\right]\quad\Longrightarrow\quad\forall a,\ M_w(a,B)=1.\]

All objects and hypotheses

{ι α β : Type*}, [Fintype ι], [MeasurableSpace α], [MeasurableSpace β] from the local section.
w : ι → ℝ≥0, independent of current state.
κ : ι → Kernel α β with [∀ i, IsMarkovKernel (κ i)].
hsum : ∑ i, w i = 1 as an equality in ℝ≥0.
There is no separate IsSFiniteKernel argument: the Markov-kernel typeclass instances supply the construction contract automatically.
No target measure, finiteness of state spaces, strict positivity of weights, nonempty-state assumption, reversibility or convergence assumption.

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

1. Express normalization in extended nonnegative arithmetic

The input weights are finite nonnegative reals but the total masses of measures are extended nonnegative reals. Apply the natural inclusion to the sum-to-one equality. This inclusion preserves finite sums and the number one, so the same normalization holds for cᵢ.

\[\sum_iw_i=1\quad\Longrightarrow\quad\sum_ic_i=\iota\!\left(\sum_iw_i\right)=\iota(1)=1.\]

Corresponding Lean step

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

The named cast lemmas are the inspected simplification support for simpa; only congrArg is written explicitly.

2. Reduce Markovness to total mass at one input

The construction already supplies a measurable kernel and therefore an output measure for every input. To prove it is Markov, fix an arbitrary input a and show that this measure assigns mass one to the full output space. No additional measurability proof or density normalization is needed.

\[\text{It remains to prove }M_w(a,B)=1\quad\text{for each }a\in A.\]

Corresponding Lean step

constructor
intro a
constructor

The two constructors unpack Markovness and then the total-mass-one field of a probability measure; their mathematical content is the stated reduction.

3. Compute the total mass and use component normalization

Evaluate the weighted-sum measure on the whole output space B. Evaluation distributes over the finite sum, and scaling a measure scales its total mass. Every component has mass one because it is Markov. Thus the mixture's mass is the sum of the weights, which equals one by the first step.

\[M_w(a,B)=\sum_i c_iK_i(a,B)=\sum_i c_i\cdot1=\sum_ic_i=1.\]

Corresponding Lean step

rw [finiteMixture_apply, Measure.finsetSum_apply]
simpa only [Measure.smul_apply, measure_univ, smul_eq_mul, mul_one] using hsum'

This finite nonnegative mass calculation proves normalization even with zero weights.

Lean statement · finiteMixture_isMarkovKernel

IsMarkovKernel says every output measure has total mass one. The bracketed ∀ i assumption supplies this property for each component. hsum is the actual normalization condition; nonnegative weights are already enforced by the type ℝ≥0. The conclusion is about the mixture kernel, not about invariance of any target measure.

theorem finiteMixture_isMarkovKernel (w : ι → ℝ≥0) (κ : ι → Kernel α β)
    [∀ i, IsMarkovKernel (κ i)] (hsum : ∑ i, w i = 1) :
    IsMarkovKernel (finiteMixture w κ)

Exact module and namespace context

Lean proof · finiteMixture_isMarkovKernel

hsum' translates the normalization equation into the number system used by measure values. After fixing a, the proof evaluates the output measure on the full space and replaces each component's mass by one. The resulting equation is hsum'.

theorem finiteMixture_isMarkovKernel (w : ι → ℝ≥0) (κ : ι → Kernel α β)
    [∀ i, IsMarkovKernel (κ i)] (hsum : ∑ i, w i = 1) :
    IsMarkovKernel (finiteMixture w κ) := by
  have hsum' : ∑ i, (w i : ℝ≥0∞) = 1 := by
    simpa using congrArg (fun r : ℝ≥0 => (r : ℝ≥0∞)) hsum
  constructor
  intro a
  constructor
  rw [finiteMixture_apply, Measure.finsetSum_apply]
  simpa only [Measure.smul_apply, measure_univ, smul_eq_mul, mul_one] using hsum'

/-- A fixed normalized finite mixture preserves any common invariant measure.

There is no finite or s-finite assumption on `μ`. The component s-finiteness is
only the `withDensity` construction contract; intended Markov components satisfy
it automatically. This statement does not extend to state-dependent weights. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Normalization alone says nothing about a common invariant measure; finiteMixture_invariant addresses that separate assertion.
Weights need not be positive. A mixture containing the identity kernel need not have positive holding probability.
Empty I cannot satisfy hsum.
No sampling implementation, state-dependent scan rule, reversibility, aperiodicity, convergence or mixing bound.
The abstract normalized-mixture theorem is source-neutral; no numbered textbook theorem is assigned.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ProbabilityTheory.IsMarkovKernel
MeasureTheory.IsProbabilityMeasure
congrArg
ENNReal.ofNNReal_finsetSum
ENNReal.coe_one
MeasureTheory.Measure.finsetSum_apply
MeasureTheory.Measure.smul_apply
MeasureTheory.IsProbabilityMeasure.measure_univ
smul_eq_mul
mul_one

Mathematical sources

ASTIS Markov-mixture theorem — Directly inspected theorem and proof.
Markov kernels are probability-valued — Definition and surrounding instance chain were inspected.
Finite sums of measures evaluate termwise — Exact finite-sum helper.
Embedding weights preserves finite sums — Exact cast simplification support.
Focused tests (consumer evidence) — Tests preserve the arbitrary-target contract; remove a zero-weight Bool component at the measure level; and use a private Bool family consisting of the identity and heatBathSnd. The latter is Markov, invariant, and reusable in invariant_pow. The identity weight may be zero, so the tests do not establish positive holding probability or aperiodicity.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

ASTIS mathematical exposition

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.

\[\left[\forall i,\ \mu K_i=\mu\right]\ \land\ \left[\sum_iw_i=1\right]\quad\Longrightarrow\quad\mu M_w=\mu,\qquad M_w(a,\cdot)=\sum_i c_iK_i(a,\cdot).\]

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

1. Put normalization into the measure-value number system

Set cᵢ to be wᵢ viewed as an extended nonnegative real. The inclusion preserves finite sums and one, so the normalized-weight equation becomes ∑ᵢcᵢ=1. This is the equation needed at the end of the measure calculation.

\[c_i=\iota(w_i),\qquad\sum_ic_i=1.\]

Corresponding Lean step

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

2. Compare the evolved measure and μ on an arbitrary measurable event

Invariance is equality of measures. It suffices to prove equality on each measurable set E. For such an E, the bind formula expresses the evolved mass as the nonnegative integral of M_w(a,E). Substitute the pointwise weighted-sum identity to obtain an integral of a finite sum.

\[(\mu M_w)(E)=\int_A M_w(a,E)\,\mu(da)=\int_A\sum_i c_iK_i(a,E)\,\mu(da).\]

Corresponding Lean step

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]

Here s is E and hs is its measurability proof. Kernel.aemeasurable follows from the measurability built into the mixture kernel.

3. Interchange the finite sum and the nonnegative integral

For each i, the kernel property makes a↦Kᵢ(a,E) measurable. Multiplication by the constant cᵢ preserves measurability. Therefore finite additivity of the nonnegative integral gives the sum of the component integrals. Because all functions are nonnegative, no signed-integral cancellation or finiteness of μ is needed.

\[\int_A\sum_i c_iK_i(a,E)\,\mu(da)=\sum_i\int_A c_iK_i(a,E)\,\mu(da).\]

Corresponding Lean step

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

The proof supplies measurability for every summand; it does not invoke dominated convergence.

4. Take each fixed weight outside and use its component's invariance

The weight cᵢ does not depend on a, so it can be taken outside the lower integral. The remaining integral is precisely the E-mass of μ evolved by Kᵢ. By common component invariance, that mass equals μ(E). Apply this reasoning separately to every summand.

\[\int_A c_iK_i(a,E)\,\mu(da)=c_i\int_A K_i(a,E)\,\mu(da)=c_i(\mu K_i)(E)=c_i\mu(E).\]

Corresponding Lean step

_ = ∑ 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]

State-independent weights are essential to this step. hκ i supplies exactly the same μ for each component.

5. Use normalization and conclude equality of measures

Factor the common nonnegative extended value μ(E) out of the finite sum. Its coefficient is one, so the result is μ(E). This identity holds even when μ(E)=∞ or some weight is zero. Since E was arbitrary among measurable sets, the evolved measure equals μ, proving invariance.

\[\sum_i c_i\mu(E)=\left(\sum_ic_i\right)\mu(E)=1\cdot\mu(E)=\mu(E),\qquad\mu M_w=\mu.\]

Corresponding Lean step

_ = μ s := by rw [← Finset.sum_mul, hsum', one_mul]

Measure extensionality opened in step 2 closes the final equality; no finite/SFinite assumption on μ entered the calculation.

Lean statement · finiteMixture_invariant

The same μ appears in every hκ i, so the theorem assumes a common invariant measure. The family of s-finite-kernel instances permits construction of finiteMixture; it is not a condition on μ. ∀ i means every component must satisfy invariance, including zero-weight components under this stated theorem. The result says exact equality after one mixture transition.

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

Exact module and namespace context

Lean proof · finiteMixture_invariant

The symbols ∫⁻ and ℝ≥0∞ make explicit that the calculation uses nonnegative extended-real integrals. ext s hs selects a measurable event; the calc chain then follows its mass through the mixture, finite-sum integration, component invariance, and weight normalization. Every equation in the mathematical proof above has a corresponding part of this chain.

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

Exact module and namespace context

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.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ProbabilityTheory.Kernel.Invariant
ProbabilityTheory.Kernel.Invariant
congrArg
ENNReal.ofNNReal_finsetSum
ENNReal.coe_one
MeasureTheory.Measure.ext
MeasureTheory.Measure.bind_apply
ProbabilityTheory.Kernel.aemeasurable
MeasureTheory.Measure.finsetSum_apply
MeasureTheory.Measure.smul_apply
smul_eq_mul
MeasureTheory.lintegral_finsetSum
ProbabilityTheory.Kernel.measurable_coe
Measurable.const_mul
Finset.sum_congr
MeasureTheory.lintegral_const_mul
Finset.sum_mul
one_mul

Mathematical sources

ASTIS fixed-mixture invariance theorem — Directly inspected theorem and proof.
Measure bind on a measurable set — Only requires measurability of the event and almost-everywhere measurability of the kernel map.
Finite-sum nonnegative integral identity — Exact linearity helper, with summand measurability.
Constant-factor nonnegative integral identity — Exact factorization helper; no finite-target hypothesis.
Focused tests (consumer evidence) — Tests preserve the arbitrary-target contract; remove a zero-weight Bool component at the measure level; and use a private Bool family consisting of the identity and heatBathSnd. The latter is Markov, invariant, and reusable in invariant_pow. The identity weight may be zero, so the tests do not establish positive holding probability or aperiodicity.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.