English
For η with a finite ν and X,Y with sub-Gaussian MGFs, the exponential of t times the sum X+Y is integrable under the product measure, with a bound depending on t.
Русский
При конечной мере ν и X,Y с подгауссовыми MGФ интеграл экспоненты экспоненты от t(X+Y) существует и ограничен.
LaTeX
$$Integrable (exp(t*(X+Y))) under (κ ⊗ η) with bound depending on t$$
Lean4
theorem integrable_exp_add_compProd {η : Kernel (Ω' × Ω) Ω''} [IsZeroOrMarkovKernel η] (hX : HasSubgaussianMGF X c κ ν)
(hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)) (t : ℝ) : Integrable (fun ω ↦ exp (t * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ∘ₘ ν) :=
by
by_cases hκ : IsSFiniteKernel κ
swap; · simp [hκ]
rcases eq_zero_or_isMarkovKernel η with rfl | hη
· simp
simp_rw [mul_add, exp_add]
refine MemLp.integrable_mul (p := 2) (q := 2) ?_ ?_
· have h := hX.memLp_exp_mul t 2
simp only [ENNReal.coe_ofNat] at h
have : κ ∘ₘ ν = ((κ ⊗ₖ η) ∘ₘ ν).map Prod.fst := by rw [Measure.map_comp _ _ measurable_fst, ← fst_eq, fst_compProd]
rwa [this, memLp_map_measure_iff h.1 measurable_fst.aemeasurable] at h
· have h := hY.memLp_exp_mul t 2
rwa [ENNReal.coe_ofNat, Measure.comp_compProd_comm, Measure.snd,
memLp_map_measure_iff h.1 measurable_snd.aemeasurable] at h
