AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixture

- A finite fixed-weight mixture, formed through constant-density kernels. Normalization is required by the correctness theorems, not the definition.

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. -/

AutoSamplingTheory/TechnicalLemmas/Probability/KernelMixture.lean:27published source at 0e31a3cda412

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

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. -/

AutoSamplingTheory/TechnicalLemmas/Probability/KernelMixture.lean:33published source at 0e31a3cda412

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

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. -/

AutoSamplingTheory/TechnicalLemmas/Probability/KernelMixture.lean:44published source at 0e31a3cda412

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

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

AutoSamplingTheory/TechnicalLemmas/Probability/KernelMixture.lean:60published source at 0e31a3cda412