# Domain of the moment-generating function #

For `X` a real random variable and `μ` a finite measure, the set `{t | Integrable (fun ω ↦ exp (t * X ω)) μ}` is an interval containing zero. This is the set of points for which the moment-generating function `mgf X μ t` is well defined. We denote that set by `integrableExpSet X μ`.

We prove the integrability of other functions for `t` in the interior of that interval.

## Main definitions #

- `ProbabilityTheory.IntegrableExpSet`: the interval of reals for which `exp (t * X)` is integrable.

## Main results #

- `ProbabilityTheory.integrable_exp_mul_of_le_of_le`: if `exp (u * X)` is integrable for `u = a` and `u = b` then it is integrable on `[a, b]`.
- `ProbabilityTheory.convex_integrableExpSet`: `integrableExpSet X μ` is a convex set.
- `ProbabilityTheory.integrable_exp_mul_of_nonpos_of_ge`: if `exp (u * X)` is integrable for `u ≤ 0` then it is integrable on `[u, 0]`.
- `ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior`: for `v` in the interior of the interval in which `exp (t * X)` is integrable, for all nonnegative `p : ℝ`, `|X| ^ p * exp (v * X)` is integrable.
- `ProbabilityTheory.memLp_of_mem_interior_integrableExpSet`: if 0 belongs to the interior of `integrableExpSet X μ`, then `X` is in `ℒp` for all finite `p`.

source
theorem ProbabilityTheory.integrable_exp_mul_of_le_of_le {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t a b : ℝ} (ha : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (a * X ω)) μ) (hb : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (b * X ω)) μ) (hat : a ≤ t) (htb : t ≤ b) :
MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ
source
theorem ProbabilityTheory.integrable_exp_mul_of_abs_le {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t u : ℝ} (hu_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (u * X ω)) μ) (hu_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (-u * X ω)) μ) (htu : |t| ≤ |u|) :
MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ

If `ω ↦ exp (u * X ω)` is integrable at `u` and `-u`, then it is integrable on `[-u, u]`.

source
theorem ProbabilityTheory.integrable_exp_mul_of_nonneg_of_le {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t u : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hu : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (u * X ω)) μ) (h_nonneg : 0 ≤ t) (htu : t ≤ u) :
MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ

If `ω ↦ exp (u * X ω)` is integrable at `u ≥ 0`, then it is integrable on `[0, u]`.

source
theorem ProbabilityTheory.integrable_exp_mul_of_nonpos_of_ge {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t u : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hu : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (u * X ω)) μ) (h_nonpos : t ≤ 0) (htu : u ≤ t) :
MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ

If `ω ↦ exp (u * X ω)` is integrable at `u ≤ 0`, then it is integrable on `[u, 0]`.

source
def ProbabilityTheory.integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) :
Set ℝ

The interval of reals `t` for which `exp (t * X)` is integrable.

Equations

- ProbabilityTheory.integrableExpSet X μ = {t : ℝ | MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ}

Instances For

source
theorem ProbabilityTheory.integrable_of_mem_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (h : t ∈ integrableExpSet X μ) :
MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ
source
theorem ProbabilityTheory.convex_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} :
Convex ℝ (integrableExpSet X μ)

`integrableExpSet X μ` is a convex subset of `ℝ` (it is an interval).

source
theorem ProbabilityTheory.aemeasurable_of_integrable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {u v : ℝ} (huv : u ≠ v) (hu_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (u * X ω)) μ) (hv_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (v * X ω)) μ) :
AEMeasurable X μ
source
theorem ProbabilityTheory.integrable_exp_mul_abs_add {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v : ℝ} (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v + t) * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v - t) * X ω)) μ) :
MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * |X ω| + v * X ω)) μ

If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then `ω ↦ exp (t * |X| + v * X)` is integrable.

source
theorem ProbabilityTheory.integrable_exp_mul_abs {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (-t * X ω)) μ) :
MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * |X ω|)) μ

If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t`, then `ω ↦ exp (t * |X ω|)` is integrable.

source
theorem ProbabilityTheory.integrable_exp_abs_mul_abs_add {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v : ℝ} (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v + t) * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v - t) * X ω)) μ) :
MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (|t| * |X ω| + v * X ω)) μ

If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then `ω ↦ exp (|t| * |X| + v * X)` is integrable.

source
theorem ProbabilityTheory.integrable_exp_abs_mul_abs {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (-t * X ω)) μ) :
MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (|t| * |X ω|)) μ

If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t`, then `ω ↦ exp (|t| * |X ω|)` is integrable.

source
theorem ProbabilityTheory.rpow_abs_le_mul_max_exp_of_pos (x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : 0 < t) :
|x| ^ p ≤ (p / t) ^ p * max (Real.exp (t * x)) (Real.exp (-t * x))

Auxiliary lemma for `rpow_abs_le_mul_max_exp`.

source
theorem ProbabilityTheory.rpow_abs_le_mul_max_exp (x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : t ≠ 0) :
|x| ^ p ≤ (p / |t|) ^ p * max (Real.exp (t * x)) (Real.exp (-t * x))
source
theorem ProbabilityTheory.rpow_abs_le_mul_exp_abs (x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : t ≠ 0) :
|x| ^ p ≤ (p / |t|) ^ p * Real.exp (|t| * |x|)
source
theorem ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v x : ℝ} (h_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v + t) * X ω)) μ) (h_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v - t) * X ω)) μ) (h_nonneg : 0 ≤ x) (hx : x < |t|) {p : ℝ} (hp : 0 ≤ p) :
MeasureTheory.Integrable (fun (a : Ω) => |X a| ^ p * Real.exp (v * X a + x * |X a|)) μ

If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable then for nonnegative `p : ℝ` and any `x ∈ [0, |t|)`, `|X| ^ p * exp (v * X + x * |X|)` is integrable.

source
theorem ProbabilityTheory.integrable_pow_abs_mul_exp_add_of_integrable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v x : ℝ} (h_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v + t) * X ω)) μ) (h_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v - t) * X ω)) μ) (h_nonneg : 0 ≤ x) (hx : x < |t|) (n : ℕ) :
MeasureTheory.Integrable (fun (a : Ω) => |X a| ^ n * Real.exp (v * X a + x * |X a|)) μ

If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable then for any `n : ℕ` and any `x ∈ [0, |t|)`, `|X| ^ n * exp (v * X + x * |X|)` is integrable.

source
theorem ProbabilityTheory.integrable_rpow_abs_mul_exp_of_integrable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v : ℝ} (ht : t ≠ 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v + t) * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v - t) * X ω)) μ) {p : ℝ} (hp : 0 ≤ p) :
MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ p * Real.exp (v * X ω)) μ

If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable then for nonnegative `p : ℝ`, `|X| ^ p * exp (v * X)` is integrable.

source
theorem ProbabilityTheory.integrable_pow_abs_mul_exp_of_integrable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v : ℝ} (ht : t ≠ 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v + t) * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v - t) * X ω)) μ) (n : ℕ) :
MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ n * Real.exp (v * X ω)) μ

If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then for all `n : ℕ`, `|X| ^ n * exp (v * X)` is integrable.

source
theorem ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v : ℝ} (ht : t ≠ 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v + t) * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v - t) * X ω)) μ) {p : ℝ} (hp : 0 ≤ p) :
MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ p * Real.exp (v * X ω)) μ

If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then for all nonnegative `p : ℝ`, `X ^ p * exp (v * X)` is integrable.

source
theorem ProbabilityTheory.integrable_pow_mul_exp_of_integrable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v : ℝ} (ht : t ≠ 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v + t) * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp ((v - t) * X ω)) μ) (n : ℕ) :
MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ n * Real.exp (v * X ω)) μ

If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then for all `n : ℕ`, `X ^ n * exp (v * X)` is integrable.

source
theorem ProbabilityTheory.integrable_rpow_abs_of_integrable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ≠ 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (-t * X ω)) μ) {p : ℝ} (hp : 0 ≤ p) :
MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ p) μ

If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ |X ω| ^ p` is integrable for all nonnegative `p : ℝ`.

source
theorem ProbabilityTheory.integrable_pow_abs_of_integrable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ≠ 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (-t * X ω)) μ) (n : ℕ) :
MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ n) μ

If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ |X ω| ^ n` is integrable for all `n : ℕ`. That is, all moments of `X` are finite.

source
theorem ProbabilityTheory.integrable_rpow_of_integrable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ≠ 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (-t * X ω)) μ) {p : ℝ} (hp : 0 ≤ p) :
MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ p) μ

If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ X ω ^ p` is integrable for all nonnegative `p : ℝ`.

source
theorem ProbabilityTheory.integrable_pow_of_integrable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ≠ 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (-t * X ω)) μ) (n : ℕ) :
MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ n) μ

If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ X ω ^ n` is integrable for all `n : ℕ`.

source
theorem ProbabilityTheory.add_half_inf_sub_mem_Ioo {l u v : ℝ} (hv : v ∈ Set.Ioo l u) :
v + min (v - l) (u - v) / 2 ∈ Set.Ioo l u
source
theorem ProbabilityTheory.sub_half_inf_sub_mem_Ioo {l u v : ℝ} (hv : v ∈ Set.Ioo l u) :
v - min (v - l) (u - v) / 2 ∈ Set.Ioo l u
source
theorem ProbabilityTheory.aemeasurable_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (hv : v ∈ interior (integrableExpSet X μ)) :
AEMeasurable X μ

If the interior of the interval `integrableExpSet X μ` is nonempty, then `X` is a.e. measurable.

source
theorem ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (hv : v ∈ interior (integrableExpSet X μ)) {p : ℝ} (hp : 0 ≤ p) :
MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ p * Real.exp (v * X ω)) μ

If `v` belongs to the interior of the interval `integrableExpSet X μ`, then `|X| ^ p * exp (v * X)` is integrable for all nonnegative `p : ℝ`.

source
theorem ProbabilityTheory.integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (hv : v ∈ interior (integrableExpSet X μ)) (n : ℕ) :
MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ n * Real.exp (v * X ω)) μ

If `v` belongs to the interior of the interval `integrableExpSet X μ`, then `|X| ^ n * exp (v * X)` is integrable for all `n : ℕ`.

source
theorem ProbabilityTheory.integrable_rpow_mul_exp_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (hv : v ∈ interior (integrableExpSet X μ)) {p : ℝ} (hp : 0 ≤ p) :
MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ p * Real.exp (v * X ω)) μ

If `v` belongs to the interior of the interval `integrableExpSet X μ`, then `X ^ p * exp (v * X)` is integrable for all nonnegative `p : ℝ`.

source
theorem ProbabilityTheory.integrable_pow_mul_exp_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (hv : v ∈ interior (integrableExpSet X μ)) (n : ℕ) :
MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ n * Real.exp (v * X ω)) μ

If `v` belongs to the interior of the interval `integrableExpSet X μ`, then `X ^ n * exp (v * X)` is integrable for all `n : ℕ`.

source
theorem ProbabilityTheory.integrable_rpow_abs_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : 0 ∈ interior (integrableExpSet X μ)) {p : ℝ} (hp : 0 ≤ p) :
MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ p) μ

If 0 belongs to the interior of the interval `integrableExpSet X μ`, then `|X| ^ n` is integrable for all nonnegative `p : ℝ`.

source
theorem ProbabilityTheory.integrable_pow_abs_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : 0 ∈ interior (integrableExpSet X μ)) (n : ℕ) :
MeasureTheory.Integrable (fun (ω : Ω) => |X ω| ^ n) μ

If 0 belongs to the interior of the interval `integrableExpSet X μ`, then `|X| ^ n` is integrable for all `n : ℕ`.

source
theorem ProbabilityTheory.integrable_rpow_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : 0 ∈ interior (integrableExpSet X μ)) {p : ℝ} (hp : 0 ≤ p) :
MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ p) μ

If 0 belongs to the interior of the interval `integrableExpSet X μ`, then `X ^ n` is integrable for all nonnegative `p : ℝ`.

source
theorem ProbabilityTheory.integrable_pow_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : 0 ∈ interior (integrableExpSet X μ)) (n : ℕ) :
MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ n) μ

If 0 belongs to the interior of the interval `integrableExpSet X μ`, then `X ^ n` is integrable for all `n : ℕ`.

source
theorem ProbabilityTheory.memLp_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : 0 ∈ interior (integrableExpSet X μ)) (p : NNReal) :
MeasureTheory.MemLp X (↑p) μ

If 0 belongs to the interior of `integrableExpSet X μ`, then `X` is in `ℒp` for all finite `p`.

source
theorem ProbabilityTheory.integrable_cexp_mul_of_re_mem_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hX : AEMeasurable X μ) (hz : z.re ∈ integrableExpSet X μ) :
MeasureTheory.Integrable (fun (ω : Ω) => Complex.exp (z * ↑(X ω))) μ
source
theorem ProbabilityTheory.integrable_cexp_mul_of_re_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)) :
MeasureTheory.Integrable (fun (ω : Ω) => Complex.exp (z * ↑(X ω))) μ
source
theorem ProbabilityTheory.integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)) {p : ℝ} (hp : 0 ≤ p) :
MeasureTheory.Integrable (fun (ω : Ω) => ↑(|X ω| ^ p) * Complex.exp (z * ↑(X ω))) μ
source
theorem ProbabilityTheory.integrable_pow_abs_mul_cexp_of_re_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) :
MeasureTheory.Integrable (fun (ω : Ω) => ↑|X ω| ^ n * Complex.exp (z * ↑(X ω))) μ
source
theorem ProbabilityTheory.integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)) {p : ℝ} (hp : 0 ≤ p) :
MeasureTheory.Integrable (fun (ω : Ω) => ↑(X ω ^ p) * Complex.exp (z * ↑(X ω))) μ
source
theorem ProbabilityTheory.integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) :
MeasureTheory.Integrable (fun (ω : Ω) => ↑(X ω) ^ n * Complex.exp (z * ↑(X ω))) μ