prodMkLeft_compProd — Mathlib

English

If Y has a sub-Gaussian mgf with respect to η and (before ω) finite ν, then the left proection under prodMkLeft retains the sub-Gaussian mgf with a product kernel.

Русский

Если Y имеет подгауссову mgf относительно η и конечна ν, то левое проецирование через prodMkLeft сохраняет mgf с произведением ядер.

LaTeX

$$HasSubgaussianMGF Y cY η (ν ⊗ₘ κ) → HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ κ)$$

Lean4

theorem prodMkLeft_compProd {η : Kernel Ω Ω''} (h : HasSubgaussianMGF Y cY η (κ ∘ₘ ν)) :
    HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ) :=
  by
  by_cases hν : SFinite ν
  swap; · simp [hν]
  by_cases hκ : IsSFiniteKernel κ
  swap; · simp [hκ]
  constructor
  · simpa using h.integrable_exp_mul
  · have h2 := h.mgf_le
    rw [← Measure.snd_compProd, Measure.snd] at h2
    exact ae_of_ae_map (by fun_prop) h2

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