`ProbabilityTheory.HasSubexponentialMGF.sum_of_hasCondSubexponentialMGF`🔗

Lemma

From the authors

Let Y be a random process adapted to a filtration ℱ, such that for all i : ℕ, Y i is conditionally sub-exponential with parameters (VY i, b) with respect to ℱ (i - 1). In particular, n ↦ ∑ i ∈ range n, Y i is a martingale. Then the sum ∑ i ∈ range n, Y i is sub-exponential with parameters (∑ i ∈ range n, VY i, b).

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

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, …

Then

HasSubexponentialMGF (fun ω => ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, VY i) 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`.

Finset.range : ℕ → Finset ℕ

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

Code

lemma HasSubexponentialMGF.sum_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 μ) :
    HasSubexponentialMGF (fun ω ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, VY i)
      b μ

Proof

by
  induction n with
  | zero => simp
  | succ n hn =>
    induction n with
    | zero => simp [h0]
    | succ n =>
      specialize hn fun i hi ↦ h_sub i (by lia)
      simp_rw [Finset.sum_range_succ _ (n + 1)]
      refine HasSubexponentialMGF.add_of_hasCondSubexponentialMGF (ℱ.le n) ?_ (h_sub n (by lia))
      refine HasSubexponentialMGF.trim (ℱ.le n) ?_ hn
      refine Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦
        (h_adapted m).mono (ℱ.mono ?_) le_rfl
      simp only [Finset.mem_range] at hm
      lia

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, 84 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.HasSubexponentialMGF.sum_of_hasCondSubexponentialMGF🔗

`ProbabilityTheory.HasSubexponentialMGF.sum_of_hasCondSubexponentialMGF`🔗