`ProbabilityTheory.measure_sum_ge_le_of_hasCondSubexponentialMGF`🔗

Lemma

From the authors

Bernstein-type inequality for sums of conditionally sub-exponential random variables.

Types

Ω : Type u_1mΩ : MeasurableSpace ΩA measurable space is a space equipped with a σ-algebra.StandardBorelSpace ΩA standard Borel space is a measurable space arising as the Borel sets of some Polish topology.

Given

μ : MeasureTheory.Measure ΩA measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.MeasureTheory.IsZeroOrProbabilityMeasure μA measure μ is zero or a probability measure if μ univ = 0 or μ univ = 1.
b : ℝ
Y : ℕ → Ω → ℝ
VY : ℕ → ℝ
ℱ : MeasureTheory.Filtration ℕ mΩA Filtration on a measurable space Ω with σ-algebra m is a monotone sequence of sub-σ-algebras of m.
n : ℕ
t : ℝ

Assuming

h_adapted : MeasureTheory.Adapted ℱ YA sequence of functions u is adapted to a filtration f if for all i, u i is f i-measurable.
h0 : HasSubexponentialMGF (Y 0) (VY 0) b μX has a sub-exponential moment generating function with parameters (V, b): for every t with b * |t| ≤ 1, exp (t * X) is integrable and mgf X μ t ≤ exp (V * t ^ 2 / 2).
h_sub : ∀ i < n - 1, HasCondSubexponentialMGF (↑ℱ i) ⋯ (Y (i + 1)) (VY (i + 1)) b μA random variable X has a conditionally sub-exponential moment-generating function with parameters (V, b) with respect to a sigma-algebra m and a measure μ if for all t with b * |t| ≤ 1, …
ht : 0 ≤ t

Then

μ.real {ω | t ≤ ∑ i ∈ Finset.range n, Y i ω} ≤ Real.exp (-min (t ^ 2 / (2 * ∑ i ∈ Finset.range n, VY i)) (t / (2 * b)))

MeasurableSpace : Type u_6 → Type u_6

A measurable space is a space equipped with a σ-algebra.

StandardBorelSpace : (α : Type u_1) → [MeasurableSpace α] → Prop

A standard Borel space is a measurable space arising as the Borel sets of some Polish topology.
This is useful in situations where a space has no natural topology or
the natural topology in a space is non-Polish.

To endow a standard Borel space `α` with a compatible Polish topology, use
`letI := upgradeStandardBorel α`. One can then use `eq_borel_upgradeStandardBorel α` to
rewrite the `MeasurableSpace α` instance to `borel α t`, where `t` is the new topology.

MeasureTheory.IsZeroOrProbabilityMeasure : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop

A measure `μ` is zero or a probability measure if `μ univ = 0` or `μ univ = 1`. This class
of measures appears naturally when conditioning on events, and many results which are true for
probability measures hold more generally over this class.

MeasureTheory.Measure : (α : Type u_5) → [MeasurableSpace α] → Type u_5

A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.

Real : Type

The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.

Nat : Type

The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

MeasureTheory.Filtration : {Ω : Type u_1} → (ι : Type u_2) → [Preorder ι] → MeasurableSpace Ω → Type (max u_1 u_2)

A `Filtration` on a measurable space `Ω` with σ-algebra `m` is a monotone
sequence of sub-σ-algebras of `m`.

MeasureTheory.Adapted : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      [inst : Preorder ι] →
        {β : ι → Type u_3} →
          [(i : ι) → MeasurableSpace (β i)] → MeasureTheory.Filtration ι m → ((i : ι) → Ω → β i) → Prop

A sequence of functions `u` is adapted to a filtration `f` if for all `i`,
`u i` is `f i`-measurable.

The definition known as `Adapted` before 2026-01-13 is now `StronglyAdapted`.

ProbabilityTheory.HasSubexponentialMGF : {Ω : Type u_1} →
  {mΩ : MeasurableSpace Ω} →
    (Ω → ℝ) → ℝ → ℝ → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasSubexponentialMGF._auto_1 → Prop

`X` has a sub-exponential moment generating function with parameters `(V, b)`: for every
`t` with `b * |t| ≤ 1`, `exp (t * X)` is integrable and `mgf X μ t ≤ exp (V * t ^ 2 / 2)`.
For `b = 0` this is `HasSubgaussianMGF X V μ`.

This is equivalent to `Kernel.HasSubexponentialMGF X V b (Kernel.const Unit μ) (Measure.dirac ())`,
as proved in `hasSubexponentialMGF_iff_kernel`.

Go to its page

ProbabilityTheory.HasCondSubexponentialMGF : {Ω : Type u_1} →
  (m : MeasurableSpace Ω) →
    {mΩ : MeasurableSpace Ω} →
      m ≤ mΩ →
        [StandardBorelSpace Ω] →
          (Ω → ℝ) →
            ℝ →
              ℝ →
                (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasCondSubexponentialMGF._auto_1) →
                  [MeasureTheory.IsFiniteMeasure μ] → Prop

A random variable `X` has a conditionally sub-exponential moment-generating function
with parameters `(V, b)` with respect to a sigma-algebra `m` and a measure `μ` if for all `t`
with `b * |t| ≤ 1`, `exp (t * X)` is `μ`-integrable and the moment-generating function of `X`
conditioned on `m` is almost surely bounded by `exp (V * t ^ 2 / 2)`.

The actual definition uses `Kernel.HasSubexponentialMGF`: `HasCondSubexponentialMGF` is defined
as sub-exponential with respect to the conditional expectation kernel for `m` and the restriction
of `μ` to the sigma-algebra `m`.

Go to its page

HSub.hSub : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HSub α β γ] → α → β → γ

`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).

HAdd.hAdd : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HAdd α β γ] → α → β → γ

`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.

LE.le : {α : Type u} → [self : LE α] → α → α → Prop

The less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

MeasureTheory.Measure.real : {α : Type u_5} → {m : MeasurableSpace α} → MeasureTheory.Measure α → Set α → ℝ

The real-valued version of a measure. Maps infinite measure sets to zero. Use as `μ.real s`.
The API is developed in `Mathlib/MeasureTheory/Measure/Real.lean`.

Set.ofPred : {α : Type u} → (α → Prop) → Set α

Turn a predicate `p : α → Prop` into a set, also written as `{x | p x}`

Finset.range : ℕ → Finset ℕ

`range n` is the set of natural numbers less than `n`.

Real.exp : ℝ → ℝ

The real exponential function, defined as the real part of the complex exponential

Neg.neg : {α : Type u} → [self : Neg α] → α → α

`-a` computes the negative or opposite of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator).

Min.min : {α : Type u} → [self : Min α] → α → α → α

Returns the lesser of its two arguments. 

Conventions for notations in identifiers:

 * The recommended spelling of `min` in identifiers is `min`.

 * The recommended spelling of `⊓` in identifiers is `inf` (`⊓` is the preferred notation for `min` when the type is not linearly ordered.).

HPow.hPow : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HPow α β γ] → α → β → γ

`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`.

HDiv.hDiv : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HDiv α β γ] → α → β → γ

`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.

HMul.hMul : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HMul α β γ] → α → β → γ

`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.

Code

lemma measure_sum_ge_le_of_hasCondSubexponentialMGF [IsZeroOrProbabilityMeasure μ]
    (h_adapted : Adapted ℱ Y) (h0 : HasSubexponentialMGF (Y 0) (VY 0) b μ) (n : ℕ)
    (h_sub : ∀ i < n - 1,
      HasCondSubexponentialMGF (ℱ i) (ℱ.le i) (Y (i + 1)) (VY (i + 1)) b μ)
    {t : ℝ} (ht : 0 ≤ t) :
    μ.real {ω | t ≤ ∑ i ∈ Finset.range n, Y i ω}
      ≤ exp (-min (t ^ 2 / (2 * ∑ i ∈ Finset.range n, VY i)) (t / (2 * b)))

Proof

(HasSubexponentialMGF.sum_of_hasCondSubexponentialMGF h_adapted h0 n h_sub).measure_ge_le ht

Meaning last changed in v4.34.0-rc2-76-g565f652 (2026-09-10).

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Audit surface: 3 project declarations, 92 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.

ProbabilityTheory.measure_sum_ge_le_of_hasCondSubexponentialMGF🔗

`ProbabilityTheory.measure_sum_ge_le_of_hasCondSubexponentialMGF`🔗