integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet

English

If X is AE-measurable and Re(z) belongs to integrableExpSet X μ, then the complex exponential cexp(z X) is integrable.

Русский

Если XAE измерима и Re(z) принадлежит integrableExpSet X μ, то cexp(z X) интегрируемо.

LaTeX

$$$\text{If } X \text{ is AEMeasurable and } \operatorname{Re}(z) \in \text{integrableExpSet}(X,\mu), \quad \mathrm{Integrable}( \lambda\omega. \mathrm{cexp}(z \cdot X(\omega)) ).$$$

Lean4

/-- If `v` belongs to the interior of the interval `integrableExpSet X μ`,
then `|X| ^ n * exp (v * X)` is integrable for all `n : ℕ`. -/
theorem integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet (hv : v ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    Integrable (fun ω ↦ |X ω| ^ n * exp (v * X ω)) μ :=
  by
  convert integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hv (by positivity : 0 ≤ (n : ℝ)) with ω
  simp

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