Theorems · Definition · probability
ProbabilityTheory.integrableExpSet
{Ω : Type u_1} → {m : MeasurableSpace Ω} → (Ω → ℝ) → MeasureTheory.Measure Ω → Set ℝThe interval of reals t for which exp (t * X) is integrable.
- Cited by
- 66 results in Mathlib
- Foundations
- Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- Set.ofPredproof · cited by 6,101
- MeasureTheory.Integrableproof · cited by 1,367
- Real.expproof · cited by 871
Cited by66
Results whose statement or proof uses this declaration.
- ProbabilityTheory.aemeasurable_of_mem_interior_integrableExpSetstatement and proof · cited by 6
- ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSetstatement and proof · cited by 5
- ProbabilityTheory.deriv_cgfstatement and proof · cited by 4
- ProbabilityTheory.analyticAt_mgfstatement and proof · cited by 4
- ProbabilityTheory.IsGaussian.memLp_idproof · cited by 4
- ProbabilityTheory.deriv_mgfstatement and proof · cited by 3
- ProbabilityTheory.differentiableAt_mgfstatement and proof · cited by 3
- ProbabilityTheory.hasDerivAt_integral_pow_mul_expstatement and proof · cited by 3
- ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_realstatement and proof · cited by 3
- ProbabilityTheory.analyticOnNhd_complexMGFstatement · cited by 3
- ProbabilityTheory.memLp_of_mem_interior_integrableExpSetstatement and proof · cited by 3
- ProbabilityTheory.integrableExpSet_eq_of_mgf'statement · cited by 2