comp_apply_univ_le — Mathlib

English

For kernels κ, η and a ∈ α, one has (η ∘ₖ κ)(a, Set.univ) ≤ κ(a, Set.univ) · η.bound.

Русский

Для ядер κ, η и элемента a ∈ α выполняется (η ∘ₖ κ)(a, Set.univ) ≤ κ(a, Set.univ) · η.bound.

LaTeX

$$$(\\eta \\circ_k \\kappa) a(\\mathrm{Set.univ}) \\le (\\kappa a)(\\mathrm{Set.univ}) \\cdot \\eta.bound$$$

Lean4

theorem comp_apply_univ_le (κ : Kernel α β) (η : Kernel β γ) (a : α) : (η ∘ₖ κ) a Set.univ ≤ κ a Set.univ * η.bound :=
  by
  rw [comp_apply' _ _ _ .univ]
  let Cη := η.bound
  calc
    ∫⁻ b, η b Set.univ ∂κ a ≤ ∫⁻ _, Cη ∂κ a := lintegral_mono fun b => measure_le_bound η b Set.univ
    _ = Cη * κ a Set.univ := (MeasureTheory.lintegral_const Cη)
    _ = κ a Set.univ * Cη := mul_comm _ _

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