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.memℒp_of_mem_interior_integrableExpSet: if 0 belongs to the interior of integrableExpSet X μ, then X is in ℒp for all finite p.

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 ω)) μ

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].

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].

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].

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 ω)) μ}

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 ω)) μ

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).

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 μ

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.

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.

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.

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.

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

Auxiliary lemma for rpow_abs_le_mul_max_exp.

theorem ProbabilityTheory.rpow_abs_le_mul_max_exp (x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : t ≠ 0) : |x| ^ p ≤ (p / |t|) ^ p * (Real.exp (t * x) ⊔ Real.exp (-t * x))

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|)

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.

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.

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.

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.

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.

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.

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 : ℝ.

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.

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 : ℝ.

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 : ℕ.

theorem ProbabilityTheory.add_half_inf_sub_mem_Ioo {l u v : ℝ} (hv : v ∈ Set.Ioo l u) : v + ((v - l) ⊓ (u - v)) / 2 ∈ Set.Ioo l u

theorem ProbabilityTheory.sub_half_inf_sub_mem_Ioo {l u v : ℝ} (hv : v ∈ Set.Ioo l u) : v - ((v - l) ⊓ (u - v)) / 2 ∈ Set.Ioo l u

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.

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 : ℝ.

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 : ℕ.

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 : ℝ.

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 : ℕ.

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 : ℝ.

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 : ℕ.

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 : ℝ.

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 : ℕ.

theorem ProbabilityTheory.memℒp_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : 0 ∈ interior (integrableExpSet X μ)) (p : NNReal) : MeasureTheory.Memℒp X (↑p) μ

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