production module

`AutoSamplingTheory.TechnicalLemmas.Probability.KernelTransport`

Read the mathematical statements and proofs in order

1 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Probability/KernelTransport.lean.

Imports

Mathlib.Probability.Kernel.Invariance external

Imported by

AutoSamplingTheory.TechnicalLemmas.Probability.CoordinateHeatBathTests.KernelTransport

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Probability.KernelTransport.invariant_map_comap Partial Not mapped

Read the complete mathematical statement and proof, with Lean below each

- Conjugating a kernel by a measurable equivalence preserves invariance of the corresponding pushforward measure. The input is pulled back with `e.symm` and the output is pushed forward with `e`. This is exact invariance only, not reversibility or convergence. The equivalence supplies genuine measurability, so no nonmeasurable-map fallback is used.

theorem invariant_map_comap {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    {κ : Kernel α α} {μ : Measure α} (e : α ≃ᵐ β) (hκ : κ.Invariant μ) :
    ((κ.comap e.symm e.symm.measurable).map e).Invariant (μ.map e) := by
  change ((κ.comap e.symm e.symm.measurable).map e) ∘ₘ μ.map e = μ.map e
  rw [← Measure.map_comp _ _ e.measurable,
    ← Kernel.comp_deterministic_eq_comap, ← Measure.comp_assoc,
    Measure.deterministic_comp_eq_map, e.map_symm_map, hκ.def]

end AutoSamplingTheory.TechnicalLemmas.Probability.KernelTransport

AutoSamplingTheory/TechnicalLemmas/Probability/KernelTransport.lean:21published source at 0e31a3cda412