`ProbabilityTheory.Kernel.HasSubexponentialMGF.add_of_holderConjugate`🔗

Lemma

From the authors

Sum of two (not necessarily independent) sub-exponential variables, by Hölder's inequality with conjugate exponents p and q. The case p = q = 2 is add.

Types

Ω : Type u_1mΩ : MeasurableSpace ΩA measurable space is a space equipped with a σ-algebra.
Ω' : Type u_2mΩ' : MeasurableSpace Ω'

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.
κ : Kernel Ω' ΩA kernel from a measurable space α to another measurable space β is a measurable function κ : α → Measure β.
X : Ω → ℝ
Y : Ω → ℝ
VX : ℝ
VY : ℝ
bX : ℝ
bY : ℝ
p : ℝ
q : ℝ

Assuming

hpq : p.HolderConjugate qReal numbers p q : ℝ are **Hölder conjugate** if they are positive and satisfy the equality p⁻¹ + q⁻¹ = 1.
hX : HasSubexponentialMGF X VX bX κ νA random variable X has a sub-exponential moment-generating function with parameters (V, b) with respect to a kernel κ and a measure ν if for every t with b * |t| ≤ 1, exp (t * X) is int…
hY : HasSubexponentialMGF Y VY bY κ ν

Then

HasSubexponentialMGF (fun ω => X ω + Y ω) (p * VX + q * VY) (max (p * bX) (q * bY)) κ ν

MeasurableSpace : Type u_6 → Type u_6

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

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

ProbabilityTheory.Kernel : (α : Type u_1) → (β : Type u_2) → [MeasurableSpace α] → [MeasurableSpace β] → Type (max u_1 u_2)

A kernel from a measurable space `α` to another measurable space `β` is a measurable function
`κ : α → Measure β`. The measurable space structure on `MeasureTheory.Measure β` is given by
`MeasureTheory.Measure.instMeasurableSpace`. A map `κ : α → MeasureTheory.Measure β` is measurable
iff `∀ s : Set β, MeasurableSet s → Measurable (fun a ↦ κ a s)`.

Real : Type

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

Real.HolderConjugate : ℝ → ℝ → Prop

Real numbers `p q : ℝ` are **Hölder conjugate** if they are positive and satisfy the
equality `p⁻¹ + q⁻¹ = 1`. This is an abbreviation for `Real.HolderTriple p q 1`. This condition
shows up in many theorems in analysis, notably related to `L^p` norms.

It is equivalent that `1 < p` and `p⁻¹ + q⁻¹ = 1`. See `Real.holderConjugate_iff`.

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

A random variable `X` has a sub-exponential moment-generating function with parameters
`(V, b)` with respect to a kernel `κ` and a measure `ν` if for every `t` with `b * |t| ≤ 1`,
`exp (t * X)` is integrable with respect to `κ ∘ₘ ν` and, for `ν`-almost all `ω'`,
the moment-generating function of `X` with respect to `κ ω'` is bounded by `exp (V * t ^ 2 / 2)`.
For `b = 0` this is `Kernel.HasSubgaussianMGF X V κ ν`.

Go to its page

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

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

Max.max : {α : Type u} → [self : Max α] → α → α → α

Returns the greater of its two arguments. 

Conventions for notations in identifiers:

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

 * The recommended spelling of `⊔` in identifiers is `sup` (`⊔` is the preferred notation for `max` when the type is not linearly ordered.).

Code

lemma add_of_holderConjugate {Y : Ω → ℝ} {VX VY bX bY p q : ℝ} (hpq : p.HolderConjugate q)
    (hX : HasSubexponentialMGF X VX bX κ ν) (hY : HasSubexponentialMGF Y VY bY κ ν) :
    HasSubexponentialMGF (fun ω ↦ X ω + Y ω) (p * VX + q * VY) (max (p * bX) (q * bY)) κ ν

Proof

by
  have hp : 0 < p := hpq.pos
  have hq : 0 < q := hpq.symm.pos
  have hpX : ∀ t, max (p * bX) (q * bY) * |t| ≤ 1 → bX * |p * t| ≤ 1 := fun t ht ↦ by
    rw [abs_mul, abs_of_pos hp]
    calc bX * (p * |t|) = (p * bX) * |t| := by ring
      _ ≤ max (p * bX) (q * bY) * |t| := by gcongr; exact le_max_left _ _
      _ ≤ 1 := ht
  have hqY : ∀ t, max (p * bX) (q * bY) * |t| ≤ 1 → bY * |q * t| ≤ 1 := fun t ht ↦ by
    rw [abs_mul, abs_of_pos hq]
    calc bY * (q * |t|) = (q * bY) * |t| := by ring
      _ ≤ max (p * bX) (q * bY) * |t| := by gcongr; exact le_max_right _ _
      _ ≤ 1 := ht
  have hp' : ((p.toNNReal : ℝ≥0) : ℝ) = p := Real.coe_toNNReal p hp.le
  have hq' : ((q.toNNReal : ℝ≥0) : ℝ) = q := Real.coe_toNNReal q hq.le
  refine ⟨fun t ht ↦ ?_, ?_⟩
  · simp_rw [mul_add, exp_add]
    have : (↑p.toNNReal : ℝ≥0∞).HolderTriple (↑q.toNNReal) 1 := hpq.ennrealOfReal
    exact MemLp.integrable_mul (hX.memLp_exp_mul p.toNNReal (by rw [hp']; exact hpX t ht))
      (hY.memLp_exp_mul q.toNNReal (by rw [hq']; exact hqY t ht))
  · filter_upwards [hX.mgf_le, hY.mgf_le, hX.ae_forall_memLp_exp_mul p.toNNReal,
      hY.ae_forall_memLp_exp_mul q.toNNReal] with ω' hmX hmY hlX hlY t ht
    calc (κ ω')[fun ω ↦ exp (t * (X ω + Y ω))]
    _ ≤ (κ ω')[fun ω ↦ exp (t * X ω) ^ p] ^ (1 / p) *
        (κ ω')[fun ω ↦ exp (t * Y ω) ^ q] ^ (1 / q) := by
      simp_rw [mul_add, exp_add]
      apply integral_mul_le_Lp_mul_Lq_of_nonneg hpq
      · exact ae_of_all _ fun _ ↦ exp_nonneg _
      · exact ae_of_all _ fun _ ↦ exp_nonneg _
      · exact hlX t (by rw [hp']; exact hpX t ht)
      · exact hlY t (by rw [hq']; exact hqY t ht)
    _ ≤ exp (VX * (t * p) ^ 2 / 2) ^ (1 / p) * exp (VY * (t * q) ^ 2 / 2) ^ (1 / q) := by
      simp_rw [← exp_mul _ p, ← exp_mul _ q, mul_right_comm t _ p, mul_right_comm t _ q]
      gcongr
      · exact hmX (t * p) (by rw [mul_comm t p]; exact hpX t ht)
      · exact hmY (t * q) (by rw [mul_comm t q]; exact hqY t ht)
    _ = exp ((p * VX + q * VY) * t ^ 2 / 2) := by
      simp_rw [← exp_mul, ← exp_add]
      congr 1
      field_simp

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: 1 project declarations, 66 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.Kernel.HasSubexponentialMGF.add_of_holderConjugate🔗

`ProbabilityTheory.Kernel.HasSubexponentialMGF.add_of_holderConjugate`🔗