aemeasurable_of_integrable_exp_mul

English

If u ≠ v and both exp(u X) and exp(v X) are μ-integrable, then X is AEMeasurable with respect to μ.

Русский

Если u ≠ v и экспоненты exp(u X) и exp(v X) обе интегрируемы по μ, то X является AEMeasurable по μ.

LaTeX

$$$\\text{AEMeasurable}(X,\\mu)$$$

Lean4

theorem aemeasurable_of_integrable_exp_mul (huv : u ≠ v) (hu_int : Integrable (fun ω ↦ exp (u * X ω)) μ)
    (hv_int : Integrable (fun ω ↦ exp (v * X ω)) μ) : AEMeasurable X μ :=
  by
  by_cases hu : u = 0
  · have hv : v ≠ 0 := ne_of_ne_of_eq huv.symm hu
    exact aemeasurable_of_aemeasurable_exp_mul hv hv_int.aemeasurable
  · exact aemeasurable_of_aemeasurable_exp_mul hu hu_int.aemeasurable

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