Theorems · Theorem · probability

ProbabilityTheory.memLp_tilted_mul

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (p : NNReal), MeasureTheory.MemLp X (↑p) (μ.tilted fun x => t * X x)

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

Cites31

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

Setstatement · cited by 53,352
Realstatement and proof · cited by 25,697
NormedAddCommGroupproof · cited by 15,752
MeasurableSpacestatement and proof · cited by 13,106
NormedSpaceproof · cited by 12,499
MeasureTheory.Measurestatement and proof · cited by 10,939
Top.topproof · cited by 9,680
NNRealstatement and proof · cited by 4,310
mul_commproof · cited by 2,262
absproof · cited by 1,814
MeasureTheory.Integrableproof · cited by 1,367
ENNReal.ofNNRealstatement and proof · cited by 1,279

Cited by1

Results whose statement or proof uses this declaration.

ProbabilityTheory.variance_tilted_mulproof · cited by 1