AutoSamplingTheory.TechnicalLemmas.Probability.KernelInvariance

- If `μ` is invariant for the one-step kernel `κ`, then it is invariant for its `n`-step kernel `κ ^ n` for every `n : ℕ`. This is an invariance statement only. It does not assert irreducibility, aperiodicity, convergence from another initial law, or a mixing rate.

theorem invariant_pow {α : Type*} [MeasurableSpace α]
    {κ : Kernel α α} {μ : Measure α}
    (hκ : κ.Invariant μ) (n : ℕ) :
    (κ ^ n).Invariant μ := by
  induction n with
  | zero =>
      change Kernel.id.Invariant μ
      exact Measure.id_comp
  | succ n ih =>
      rw [pow_succ]
      change ((κ ^ n) ∘ₖ κ).Invariant μ
      exact ih.comp hκ

/-- Measure-level form of `invariant_pow`: starting an invariant law and taking
`n` transitions leaves the law unchanged. -/

AutoSamplingTheory/TechnicalLemmas/Probability/KernelInvariance.lean:31published source at 0e31a3cda412Open detailed card

- Measure-level form of `invariant_pow`: starting an invariant law and taking `n` transitions leaves the law unchanged.

theorem bind_pow_eq {α : Type*} [MeasurableSpace α]
    {κ : Kernel α α} {μ : Measure α}
    (hκ : κ.Invariant μ) (n : ℕ) :
    μ.bind (κ ^ n) = μ :=
  (invariant_pow hκ n).def

end KernelInvariance
end Probability
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Probability/KernelInvariance.lean:46published source at 0e31a3cda412