integrable_of_mem_integrableExpSet

English

The set of real numbers t for which the exponential integrand exp(t X) is μ-integrable is a convex subset of R (indeed an interval).

Русский

Множество действительных чисел t, для которых интегрируемость экспоненты exp(t X) по μ выполняется, является выпуклым подмножество R (то есть интервал).

LaTeX

$$\\text{Convex}(\\mathbb{R}, \\operatorname{integrableExpSet}(X, \\mu))$$

Lean4

theorem integrable_of_mem_integrableExpSet (h : t ∈ integrableExpSet X μ) : Integrable (fun ω ↦ exp (t * X ω)) μ :=
  h

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