test module

`Tests.KernelMixture`

1 named declarations scanned from Tests/KernelMixture.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixtureAutoSamplingTheory.TechnicalLemmas.Probability.HeatBathAutoSamplingTheory.TechnicalLemmas.Probability.KernelInvariance

Imported by

No local reverse import.

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.Tests.KernelMixture.lazyHeatBathComponents Partial Not mapped

No declaration docstring.

private noncomputable def lazyHeatBathComponents (μ : Measure (α × β))
    [IsFiniteMeasure μ] (b : Bool) : Kernel (α × β) (α × β) :=
  if b then Kernel.id else HeatBath.heatBathSnd μ

private instance (μ : Measure (α × β)) [IsFiniteMeasure μ] (b : Bool) :
    IsMarkovKernel (lazyHeatBathComponents μ b) := by
  cases b <;> dsimp [lazyHeatBathComponents] <;> infer_instance

example (μ : Measure (α × β)) [IsFiniteMeasure μ] (w : Bool → ℝ≥0)
    (hsum : ∑ b, w b = 1) : IsMarkovKernel (finiteMixture w (lazyHeatBathComponents μ)) :=
  finiteMixture_isMarkovKernel w (lazyHeatBathComponents μ) hsum

-- Identity/heat-bath is a concrete lazy-update consumer; zero weights remain
-- possible. Finite iteration reuses invariant_pow, not a new wrapper theorem.
example (μ : Measure (α × β)) [IsFiniteMeasure μ] (w : Bool → ℝ≥0)
    (hsum : ∑ b, w b = 1) (n : ℕ) :
    ((finiteMixture w (lazyHeatBathComponents μ)) ^ n).Invariant μ := by
  apply KernelInvariance.invariant_pow
  apply finiteMixture_invariant w (lazyHeatBathComponents μ) μ hsum
  intro b
  cases b
  · exact HeatBath.heatBathSnd_invariant μ
  · exact Measure.id_comp

end AutoSamplingTheory.Tests.KernelMixture

Tests/KernelMixture.lean:26published source at 0e31a3cda412