Theorems · Theorem · probability

ProbabilityTheory.IsGaussian.memLp_two_fun_id

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E],
  MeasureTheory.MemLp (fun x => x) 2 μ

Eta-expanded form of ProbabilityTheory.IsGaussian.memLp_two_id

Defined in: Mathlib.Probability.Distributions.Gaussian.Fernique
Cited by: 0 results in Mathlib
Foundations: Depth 312 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup NormedSpace MeasurableSpace BorelSpace ProbabilityTheory.IsGaussian CompleteSpace SecondCountableTopology

Mathlib docs Source Loogle LeanSearch

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 · cited by 25,697
NormedAddCommGroupstatement · cited by 15,752
MeasurableSpacestatement · cited by 13,106
NormedSpacestatement · cited by 12,499
MeasureTheory.Measurestatement · cited by 10,939
ENNRealstatement · cited by 9,879
CompleteSpacestatement · cited by 2,532
BorelSpacestatement · cited by 1,602
SecondCountableTopologystatement · cited by 750
MeasureTheory.MemLpstatement · cited by 457
ProbabilityTheory.IsGaussianstatement · cited by 48
ProbabilityTheory.IsGaussian.memLp_two_idproof · cited by 10

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.