ProbabilityTheory.BrownianReal.integral_eval_projectiveFamily

∀ (I : Finset NNReal) (s : ↥I), ∫ (x : ↥I → ℝ), x s ∂ProbabilityTheory.BrownianReal.projectiveFamily I = 0

Defined in: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
Cited by: 2 results in Mathlib
Foundations: Depth 318 from the axioms · uses propext, Classical.choice, Quot.sound

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

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

DFunLike.coeproof · cited by 62,936
Realstatement and proof · cited by 25,697
Finsetstatement and proof · cited by 13,712
NNRealstatement and proof · cited by 4,310
MeasureTheory.integralstatement and proof · cited by 1,779
map_zeroproof · cited by 1,614
ContinuousLinearMap.projproof · cited by 77
ProbabilityTheory.BrownianReal.projectiveFamilystatement and proof · cited by 19
ProbabilityTheory.IsGaussian.integrable_idproof · cited by 11
ContinuousLinearMap.integral_comp_id_commproof · cited by 6
ProbabilityTheory.BrownianReal.integral_id_projectiveFamilyproof · cited by 3

Results whose statement or proof uses this declaration.