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.

theorem ProbabilityTheory.integrable_exp_mul_of_le_of_le {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} {t a b : Real} (ha : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul a (X ω))) μ) (hb : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul b (X ω))) μ) (hat : LE.le a t) (htb : LE.le t b) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul t (X ω))) μ

theorem ProbabilityTheory.integrable_exp_mul_of_abs_le {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} {t u : Real} (hu_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul u (X ω))) μ) (hu_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (Neg.neg u) (X ω))) μ) (htu : LE.le (abs t) (abs u)) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t u : Real} [MeasureTheory.IsFiniteMeasure μ] (hu : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul u (X ω))) μ) (h_nonneg : LE.le 0 t) (htu : LE.le t u) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t u : Real} [MeasureTheory.IsFiniteMeasure μ] (hu : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul u (X ω))) μ) (h_nonpos : LE.le t 0) (htu : LE.le u t) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul 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 : Ω → Real) (μ : MeasureTheory.Measure Ω) : Set Real

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

Equations

• Eq (ProbabilityTheory.integrableExpSet X μ) (setOf fun (t : Real) => MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul t (X ω))) μ)

theorem ProbabilityTheory.integrable_of_mem_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} {t : Real} (h : Membership.mem (integrableExpSet X μ) t) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul t (X ω))) μ

theorem ProbabilityTheory.convex_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} : Convex Real (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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {u v : Real} (huv : Ne u v) (hu_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul u (X ω))) μ) (hv_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul v (X ω))) μ) : AEMeasurable X μ

theorem ProbabilityTheory.integrable_exp_mul_abs_add {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} {t v : Real} (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HAdd.hAdd v t) (X ω))) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HSub.hSub v t) (X ω))) μ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HAdd.hAdd (HMul.hMul t (abs (X ω))) (HMul.hMul 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t : Real} (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul t (X ω))) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (Neg.neg t) (X ω))) μ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul t (abs (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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t v : Real} (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HAdd.hAdd v t) (X ω))) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HSub.hSub v t) (X ω))) μ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HAdd.hAdd (HMul.hMul (abs t) (abs (X ω))) (HMul.hMul 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t : Real} (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul t (X ω))) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (Neg.neg t) (X ω))) μ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (abs t) (abs (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 : Real) {t p : Real} (hp : LE.le 0 p) (ht : LT.lt 0 t) : LE.le (HPow.hPow (abs x) p) (HMul.hMul (HPow.hPow (HDiv.hDiv p t) p) (Max.max (Real.exp (HMul.hMul t x)) (Real.exp (HMul.hMul (Neg.neg t) x))))

Auxiliary lemma for rpow_abs_le_mul_max_exp.

theorem ProbabilityTheory.rpow_abs_le_mul_max_exp (x : Real) {t p : Real} (hp : LE.le 0 p) (ht : Ne t 0) : LE.le (HPow.hPow (abs x) p) (HMul.hMul (HPow.hPow (HDiv.hDiv p (abs t)) p) (Max.max (Real.exp (HMul.hMul t x)) (Real.exp (HMul.hMul (Neg.neg t) x))))

theorem ProbabilityTheory.rpow_abs_le_mul_exp_abs (x : Real) {t p : Real} (hp : LE.le 0 p) (ht : Ne t 0) : LE.le (HPow.hPow (abs x) p) (HMul.hMul (HPow.hPow (HDiv.hDiv p (abs t)) p) (Real.exp (HMul.hMul (abs t) (abs x))))

theorem ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} {t v x : Real} (h_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HAdd.hAdd v t) (X ω))) μ) (h_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HSub.hSub v t) (X ω))) μ) (h_nonneg : LE.le 0 x) (hx : LT.lt x (abs t)) {p : Real} (hp : LE.le 0 p) : MeasureTheory.Integrable (fun (a : Ω) => HMul.hMul (HPow.hPow (abs (X a)) p) (Real.exp (HAdd.hAdd (HMul.hMul v (X a)) (HMul.hMul x (abs (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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t v x : Real} (h_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HAdd.hAdd v t) (X ω))) μ) (h_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HSub.hSub v t) (X ω))) μ) (h_nonneg : LE.le 0 x) (hx : LT.lt x (abs t)) (n : Nat) : MeasureTheory.Integrable (fun (a : Ω) => HMul.hMul (HPow.hPow (abs (X a)) n) (Real.exp (HAdd.hAdd (HMul.hMul v (X a)) (HMul.hMul x (abs (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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t v : Real} (ht : Ne t 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HAdd.hAdd v t) (X ω))) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HSub.hSub v t) (X ω))) μ) {p : Real} (hp : LE.le 0 p) : MeasureTheory.Integrable (fun (ω : Ω) => HMul.hMul (HPow.hPow (abs (X ω)) p) (Real.exp (HMul.hMul 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t v : Real} (ht : Ne t 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HAdd.hAdd v t) (X ω))) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HSub.hSub v t) (X ω))) μ) (n : Nat) : MeasureTheory.Integrable (fun (ω : Ω) => HMul.hMul (HPow.hPow (abs (X ω)) n) (Real.exp (HMul.hMul 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t v : Real} (ht : Ne t 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HAdd.hAdd v t) (X ω))) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HSub.hSub v t) (X ω))) μ) {p : Real} (hp : LE.le 0 p) : MeasureTheory.Integrable (fun (ω : Ω) => HMul.hMul (HPow.hPow (X ω) p) (Real.exp (HMul.hMul 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t v : Real} (ht : Ne t 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HAdd.hAdd v t) (X ω))) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (HSub.hSub v t) (X ω))) μ) (n : Nat) : MeasureTheory.Integrable (fun (ω : Ω) => HMul.hMul (HPow.hPow (X ω) n) (Real.exp (HMul.hMul 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t : Real} (ht : Ne t 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul t (X ω))) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (Neg.neg t) (X ω))) μ) {p : Real} (hp : LE.le 0 p) : MeasureTheory.Integrable (fun (ω : Ω) => HPow.hPow (abs (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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t : Real} (ht : Ne t 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul t (X ω))) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (Neg.neg t) (X ω))) μ) (n : Nat) : MeasureTheory.Integrable (fun (ω : Ω) => HPow.hPow (abs (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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t : Real} (ht : Ne t 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul t (X ω))) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (Neg.neg t) (X ω))) μ) {p : Real} (hp : LE.le 0 p) : MeasureTheory.Integrable (fun (ω : Ω) => HPow.hPow (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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {t : Real} (ht : Ne t 0) (ht_int_pos : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul t (X ω))) μ) (ht_int_neg : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (HMul.hMul (Neg.neg t) (X ω))) μ) (n : Nat) : MeasureTheory.Integrable (fun (ω : Ω) => HPow.hPow (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 : Real} (hv : Membership.mem (Set.Ioo l u) v) : Membership.mem (Set.Ioo l u) (HAdd.hAdd v (HDiv.hDiv (Min.min (HSub.hSub v l) (HSub.hSub u v)) 2))

theorem ProbabilityTheory.sub_half_inf_sub_mem_Ioo {l u v : Real} (hv : Membership.mem (Set.Ioo l u) v) : Membership.mem (Set.Ioo l u) (HSub.hSub v (HDiv.hDiv (Min.min (HSub.hSub v l) (HSub.hSub u v)) 2))

theorem ProbabilityTheory.aemeasurable_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} {v : Real} (hv : Membership.mem (interior (integrableExpSet X μ)) v) : 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {v : Real} (hv : Membership.mem (interior (integrableExpSet X μ)) v) {p : Real} (hp : LE.le 0 p) : MeasureTheory.Integrable (fun (ω : Ω) => HMul.hMul (HPow.hPow (abs (X ω)) p) (Real.exp (HMul.hMul 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {v : Real} (hv : Membership.mem (interior (integrableExpSet X μ)) v) (n : Nat) : MeasureTheory.Integrable (fun (ω : Ω) => HMul.hMul (HPow.hPow (abs (X ω)) n) (Real.exp (HMul.hMul 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {v : Real} (hv : Membership.mem (interior (integrableExpSet X μ)) v) {p : Real} (hp : LE.le 0 p) : MeasureTheory.Integrable (fun (ω : Ω) => HMul.hMul (HPow.hPow (X ω) p) (Real.exp (HMul.hMul 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} {v : Real} (hv : Membership.mem (interior (integrableExpSet X μ)) v) (n : Nat) : MeasureTheory.Integrable (fun (ω : Ω) => HMul.hMul (HPow.hPow (X ω) n) (Real.exp (HMul.hMul 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 : Ω → Real} {μ : MeasureTheory.Measure Ω} (h : Membership.mem (interior (integrableExpSet X μ)) 0) {p : Real} (hp : LE.le 0 p) : MeasureTheory.Integrable (fun (ω : Ω) => HPow.hPow (abs (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 : Ω → Real} {μ : MeasureTheory.Measure Ω} (h : Membership.mem (interior (integrableExpSet X μ)) 0) (n : Nat) : MeasureTheory.Integrable (fun (ω : Ω) => HPow.hPow (abs (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 : Ω → Real} {μ : MeasureTheory.Measure Ω} (h : Membership.mem (interior (integrableExpSet X μ)) 0) {p : Real} (hp : LE.le 0 p) : MeasureTheory.Integrable (fun (ω : Ω) => HPow.hPow (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 : Ω → Real} {μ : MeasureTheory.Measure Ω} (h : Membership.mem (interior (integrableExpSet X μ)) 0) (n : Nat) : MeasureTheory.Integrable (fun (ω : Ω) => HPow.hPow (X ω) n) μ

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

theorem ProbabilityTheory.memLp_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} (h : Membership.mem (interior (integrableExpSet X μ)) 0) (p : NNReal) : MeasureTheory.MemLp X (ENNReal.ofNNReal p) μ

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

@[deprecated ProbabilityTheory.memLp_of_mem_interior_integrableExpSet (since := "2025-02-21")]

theorem ProbabilityTheory.memℒp_of_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} (h : Membership.mem (interior (integrableExpSet X μ)) 0) (p : NNReal) : MeasureTheory.MemLp X (ENNReal.ofNNReal p) μ

Alias of ProbabilityTheory.memLp_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_cexp_mul_of_re_mem_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} {z : Complex} (hX : AEMeasurable X μ) (hz : Membership.mem (integrableExpSet X μ) z.re) : MeasureTheory.Integrable (fun (ω : Ω) => Complex.exp (HMul.hMul z (Complex.ofReal (X ω)))) μ

theorem ProbabilityTheory.integrable_cexp_mul_of_re_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} {z : Complex} (hz : Membership.mem (interior (integrableExpSet X μ)) z.re) : MeasureTheory.Integrable (fun (ω : Ω) => Complex.exp (HMul.hMul z (Complex.ofReal (X ω)))) μ

theorem ProbabilityTheory.integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} {z : Complex} (hz : Membership.mem (interior (integrableExpSet X μ)) z.re) {p : Real} (hp : LE.le 0 p) : MeasureTheory.Integrable (fun (ω : Ω) => HMul.hMul (Complex.ofReal (HPow.hPow (abs (X ω)) p)) (Complex.exp (HMul.hMul z (Complex.ofReal (X ω))))) μ

theorem ProbabilityTheory.integrable_pow_abs_mul_cexp_of_re_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} {z : Complex} (hz : Membership.mem (interior (integrableExpSet X μ)) z.re) (n : Nat) : MeasureTheory.Integrable (fun (ω : Ω) => HMul.hMul (HPow.hPow (Complex.ofReal (abs (X ω))) n) (Complex.exp (HMul.hMul z (Complex.ofReal (X ω))))) μ

theorem ProbabilityTheory.integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} {z : Complex} (hz : Membership.mem (interior (integrableExpSet X μ)) z.re) {p : Real} (hp : LE.le 0 p) : MeasureTheory.Integrable (fun (ω : Ω) => HMul.hMul (Complex.ofReal (HPow.hPow (X ω) p)) (Complex.exp (HMul.hMul z (Complex.ofReal (X ω))))) μ

theorem ProbabilityTheory.integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → Real} {μ : MeasureTheory.Measure Ω} {z : Complex} (hz : Membership.mem (interior (integrableExpSet X μ)) z.re) (n : Nat) : MeasureTheory.Integrable (fun (ω : Ω) => HMul.hMul (HPow.hPow (Complex.ofReal (X ω)) n) (Complex.exp (HMul.hMul z (Complex.ofReal (X ω))))) μ