test module

`Tests.KernelInvariance`

0 named declarations scanned from Tests/KernelInvariance.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Probability.KernelInvariance

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

Tests/KernelInvariance.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Probability.KernelInvariance

namespace AutoSamplingTheory.Tests.KernelInvariance

open MeasureTheory
open ProbabilityTheory
open AutoSamplingTheory.TechnicalLemmas.Probability.KernelInvariance

variable {α : Type*} [MeasurableSpace α]

example {κ : Kernel α α} {μ : Measure α}
    (hκ : κ.Invariant μ) :
    (κ ^ 7).Invariant μ := by
  exact invariant_pow hκ 7

example {κ : Kernel α α} [IsMarkovKernel κ] {μ : Measure α}
    (hrev : κ.IsReversible μ) :
    μ.bind (κ ^ (5 : ℕ) : Kernel α α) = μ := by
  exact bind_pow_eq hrev.invariant 5

end AutoSamplingTheory.Tests.KernelInvariance