`ProbabilityTheory.HasCondSubexponentialMGF.mgf_le`🔗

Lemma

No docstring.

Types

Ω : Type u_1m : MeasurableSpace ΩA measurable space is a space equipped with a σ-algebra.mΩ : MeasurableSpace Ω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.IsFiniteMeasure μA measure μ is called finite if μ univ < ∞.
X : Ω → ℝ
V : ℝ
b : ℝ

Assuming

hm : m ≤ mΩimplicit
h : HasCondSubexponentialMGF m hm X V 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

∀ᵐ (ω' : Ω) ∂μ.trim hm, ∀ (t : ℝ), b * |t| ≤ 1 → mgf X ((condExpKernel μ m) ω') t ≤ Real.exp (V * t ^ 2 / 2)

f.Eventually p or ∀ᶠ x in f, p x mean that {x | p x} ∈ f.

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.IsFiniteMeasure : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop

A measure `μ` is called finite if `μ univ < ∞`.

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.

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

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

Filter.Eventually : {α : Type u_1} → (α → Prop) → Filter α → Prop

`f.Eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in atTop, p x`
means that `p` holds true for sufficiently large `x`.

MeasureTheory.Measure.trim : {α : Type u_1} → {m m0 : MeasurableSpace α} → MeasureTheory.Measure α → m ≤ m0 → MeasureTheory.Measure α

Restriction of a measure to a sub-σ-algebra.
It is common to see a measure `μ` on a measurable space structure `m0` as being also a measure on
any `m ≤ m0`. Since measures in mathlib have to be trimmed to the measurable space, `μ` itself
cannot be a measure on `m`, hence the definition of `μ.trim hm`.

This notion is related to `OuterMeasure.trim`, see the lemma
`toOuterMeasure_trim_eq_trim_toOuterMeasure`.

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

abs : {α : Type u_1} → [Lattice α] → [AddGroup α] → α → α

`abs a`, denoted `|a|`, is the absolute value of `a`

ProbabilityTheory.mgf : {Ω : Type u_1} → {m : MeasurableSpace Ω} → (Ω → ℝ) → MeasureTheory.Measure Ω → ℝ → ℝ

Moment-generating function of a real random variable `X`: `fun t => μ[exp(t*X)]`.

ProbabilityTheory.condExpKernel : {Ω : Type u_3} →
  [mΩ : MeasurableSpace Ω] →
    [StandardBorelSpace Ω] →
      (μ : MeasureTheory.Measure Ω) →
        [MeasureTheory.IsFiniteMeasure μ] → (m : MeasurableSpace Ω) → ProbabilityTheory.Kernel Ω Ω

Kernel associated with the conditional expectation with respect to a σ-algebra. It satisfies
`μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condExpKernel μ m ω)`.
It is defined as the conditional distribution of the identity given the identity, where the second
identity is understood as a map from `Ω` with the σ-algebra `mΩ` to `Ω` with σ-algebra `m ⊓ mΩ`.
We use `m ⊓ mΩ` instead of `m` to ensure that it is a sub-σ-algebra of `mΩ`. We then use
`Kernel.comap` to get a kernel from `m` to `mΩ` instead of from `m ⊓ mΩ` to `mΩ`.

Real.exp : ℝ → ℝ

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

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

Code

lemma mgf_le (h : HasCondSubexponentialMGF m hm X V b μ) :
    ∀ᵐ ω' ∂(μ.trim hm), ∀ t, b * |t| ≤ 1 →
      mgf X (condExpKernel μ m ω') t ≤ exp (V * t ^ 2 / 2)

Proof

Kernel.HasSubexponentialMGF.mgf_le h

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: 2 project declarations, 65 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.HasCondSubexponentialMGF.mgf_le🔗

`ProbabilityTheory.HasCondSubexponentialMGF.mgf_le`🔗