Exponential moments of a statistic that is bounded below

Mathlib's ProbabilityTheory.integrable_exp_mul_of_le makes exp (t * X) integrable against a finite measure when X is bounded above and the rate t is nonnegative. A law carried by a half-line [b, ∞) needs the mirror image: X bounded below and t nonpositive. Both bounds are one-sided, so neither statement follows from the two-sided ProbabilityTheory.integrable_exp_mul_of_mem_Icc.

For such a law the remaining question is which positive rates survive, and that is decided by the tail: if X already has an infinite moment of some order, then no positive rate is integrable either, because an exponential moment on both sides of the origin forces every moment to be finite. Combining the two statements gives the exponential-moment domain of a heavy-tailed half-line law, which is Set.Iic 0.

Main results

• TauCeti.integrable_exp_mul_of_ge — every nonpositive rate is integrable when X is bounded below;
• TauCeti.isFiniteMeasure_of_integrable_exp_mul — a statistic bounded below with an integrable exponential at a nonnegative rate lives on a finite measure;
• TauCeti.not_integrable_exp_mul_of_not_integrable_rpow and TauCeti.not_integrable_exp_mul_of_not_integrable_pow — no positive rate is integrable once a real, respectively natural, moment of X fails to exist;
• TauCeti.integrableExpSet_eq_Iic_of_not_integrable_pow — a statistic bounded below with an infinite natural moment has exponential-integrability domain Set.Iic 0.

theorem TauCeti.integrable_exp_mul_of_ge {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (t b : ℝ) (ht : t ≤ 0) (hX : AEMeasurable X μ) (hb : ∀ᵐ (ω : Ω) ∂μ, b ≤ X ω) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ

A nonpositive exponential rate is integrable when the statistic is bounded below. On b ≤ X the integrand exp (t * X) is at most exp (t * b) for t ≤ 0, which a finite measure integrates. This is the mirror image of ProbabilityTheory.integrable_exp_mul_of_le, which bounds X above and asks for a nonnegative rate.

theorem TauCeti.isFiniteMeasure_of_integrable_exp_mul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {b t : ℝ} (hb : ∀ᵐ (ω : Ω) ∂μ, b ≤ X ω) (ht : 0 ≤ t) (hexp : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : MeasureTheory.IsFiniteMeasure μ

A statistic bounded below with an integrable exponential at a nonnegative rate lives on a finite measure: the exponential is bounded below by a positive constant.

theorem TauCeti.not_integrable_exp_mul_of_not_integrable_rpow {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {b t : ℝ} (q : ℝ) (hb : ∀ᵐ (ω : Ω) ∂μ, b ≤ X ω) (hq : 0 ≤ q) (hmom : ¬MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ q) μ) (ht : 0 < t) : ¬MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ

A statistic bounded below whose moment of order q is infinite has no positive exponential moment. The nonpositive rates cost nothing here, so a positive rate would give exponential integrability on both sides of the origin, and that makes every moment finite.

theorem TauCeti.not_integrable_exp_mul_of_not_integrable_pow {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {b t : ℝ} (n : ℕ) (hb : ∀ᵐ (ω : Ω) ∂μ, b ≤ X ω) (hmom : ¬MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ n) μ) (ht : 0 < t) : ¬MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ

A statistic bounded below whose n-th moment is infinite has no positive exponential moment, the natural-power form of TauCeti.not_integrable_exp_mul_of_not_integrable_rpow.

theorem TauCeti.integrableExpSet_eq_Iic_of_not_integrable_pow {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] {b : ℝ} (hX : AEMeasurable X μ) (hb : ∀ᵐ (ω : Ω) ∂μ, b ≤ X ω) (n : ℕ) (hn : ¬MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ n) μ) : ProbabilityTheory.integrableExpSet X μ = Set.Iic 0

A statistic bounded below with a nonintegrable natural power has exponential moments exactly at nonpositive rates.