HasSubgaussianMGF_congr — Mathlib

English

The of_map construction preserves HasSubgaussianMGF under measurable Y with respect to ν; i.e., if h holds for κ.map Y then it holds for X∘Y with κ and ν.

Русский

Конструкция of_map сохраняет HasSubgaussianMGF при измеримом Y: если h применимо к κ.map Y, ν, то тоже к X∘Y, κ, ν.

LaTeX

$$$\\text{of_map}\\; (hY: \\text{Measurable }Y) \\; (h: \\mathrm{HasSubgaussianMGF}(X,c,\\kappa.map Y,\\nu)) \\,:\\; \\mathrm{HasSubgaussianMGF}(X\\circ Y,c,\\kappa,\\nu).$$$

Lean4

theorem _root_.ProbabilityTheory.Kernel.HasSubgaussianMGF_congr {Y : Ω → ℝ} (h : X =ᵐ[κ ∘ₘ ν] Y) :
    HasSubgaussianMGF X c κ ν ↔ HasSubgaussianMGF Y c κ ν :=
  ⟨fun hX ↦ congr hX h, fun hY ↦ congr hY (ae_eq_symm h)⟩

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