Theorems · Theorem · probability

ProbabilityTheory.Kernel.HasSubgaussianMGF.add

∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X Y : Ω → ℝ} {cX cY : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X cX κ ν →
    ProbabilityTheory.Kernel.HasSubgaussianMGF Y cY κ ν →
      ProbabilityTheory.Kernel.HasSubgaussianMGF (fun ω => X ω + Y ω) ((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) κ ν

Defined in: Mathlib.Probability.Moments.SubGaussian
Cited by: 1 results in Mathlib
Foundations: Depth 266 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites67

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
TopologicalSpaceproof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
NNRealstatement and proof · cited by 4,310
mul_oneproof · cited by 3,885
one_mulproof · cited by 2,841
add_zeroproof · cited by 2,707
Nat.cast_oneproof · cited by 2,501
zero_addproof · cited by 2,366
Nat.cast_zeroproof · cited by 1,870

Cited by1

Results whose statement or proof uses this declaration.

ProbabilityTheory.HasSubgaussianMGF.addproof · cited by 0