Theorems · Theorem · probability

ProbabilityTheory.HasSubgaussianMGF.id_map_iff

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  AEMeasurable X μ →
    (ProbabilityTheory.HasSubgaussianMGF id c (MeasureTheory.Measure.map X μ) ↔
      ProbabilityTheory.HasSubgaussianMGF X c μ)

Defined in: Mathlib.Probability.Moments.SubGaussian
Cited by: 1 results in Mathlib
Foundations: Depth 257 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.

Cites19

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

Realstatement and proof · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
NNRealstatement and proof · cited by 4,310
NNReal.toRealproof · cited by 1,260
Real.expproof · cited by 871
MeasureTheory.Measure.mapstatement and proof · cited by 858
AEMeasurablestatement and proof · cited by 840
continuous_id'proof · cited by 295
Continuous.comp_aestronglyMeasurableproof · cited by 77
ProbabilityTheory.HasSubgaussianMGFstatement and proof · cited by 36
aestronglyMeasurable_idproof · cited by 35

Cited by1

Results whose statement or proof uses this declaration.

ProbabilityTheory.HasSubgaussianMGF.congr_identDistribproof · cited by 0