const_comp — Mathlib

English

If κ is a Markov kernel, then (const β μ) ∘ κ = (const α μ).

Русский

Если κ — Марковское ядро, тогда (const β μ) ∘ κ = const α μ.

LaTeX

$$$(\\text{const } β μ) \\circ κ = \\text{const } α μ$$$

Lean4

theorem const_comp (μ : Measure γ) (κ : Kernel α β) : const β μ ∘ₖ κ = fun a ↦ (κ a) Set.univ • μ :=
  by
  ext _ _ hs
  simp_rw [comp_apply' _ _ _ hs, const_apply, MeasureTheory.lintegral_const, Measure.smul_apply, smul_eq_mul, mul_comm]

Похожие утверждения