Theorems · Theorem · probability
ProbabilityTheory.HasGaussianLaw.memLp_two
∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
[inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] [CompleteSpace E]
[SecondCountableTopology E], ProbabilityTheory.HasGaussianLaw X P → MeasureTheory.MemLp X 2 P- Cited by
- 13 results in Mathlib
- Foundations
- Depth 312 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- NormedAddCommGroupstatement and proof · cited by 15,752
- MeasurableSpacestatement and proof · cited by 13,106
- NormedSpacestatement and proof · cited by 12,499
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ENNRealstatement · cited by 9,879
- CompleteSpacestatement and proof · cited by 2,532
- BorelSpacestatement and proof · cited by 1,602
- SecondCountableTopologystatement and proof · cited by 750
- MeasureTheory.MemLpstatement · cited by 457
- ProbabilityTheory.HasGaussianLawstatement and proof · cited by 67
- ProbabilityTheory.HasGaussianLaw.memLpproof · cited by 2
Cited by13
Results whose statement or proof uses this declaration.
- ProbabilityTheory.IsGaussianProcess.isPreBrownianReal_of_covarianceproof · cited by 4
- ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_strongDualproof · cited by 3
- ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_strongDualproof · cited by 3
- ProbabilityTheory.IsGaussianProcess.indepFun_of_covariance_strongDualproof · cited by 1
- ProbabilityTheory.HasIndepIncrements.isPreBrownianReal_of_hasLawproof · cited by 1
- ProbabilityTheory.IsPreBrownianReal.shiftproof · cited by 1
- ProbabilityTheory.IsPreBrownianReal.hasIndepIncrementsproof · cited by 1
- ProbabilityTheory.IndepFun.hasGaussianLaw_sub_of_subproof · cited by 1
- ProbabilityTheory.IsGaussianProcess.iIndepFun_of_covariance_strongDualproof · cited by 1
- ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_evalproof · cited by 0
- ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_evalproof · cited by 0