ProbabilityTheory.BrownianReal.variance_eval_projectiveFamily

∀ {I : Finset NNReal} (s : ↥I),
  ProbabilityTheory.variance (fun x => x s) (ProbabilityTheory.BrownianReal.projectiveFamily I) = ↑↑s

Defined in: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
Cited by: 2 results in Mathlib
Foundations: Depth 320 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.

Realstatement and proof · cited by 25,697
Finsetstatement and proof · cited by 13,712
NNRealstatement and proof · cited by 4,310
NNReal.toRealstatement and proof · cited by 1,260
ProbabilityTheory.variancestatement · cited by 104
aemeasurable_idproof · cited by 66
min_selfproof · cited by 27
ProbabilityTheory.BrownianReal.projectiveFamilystatement · cited by 19
ProbabilityTheory.covariance_selfproof · cited by 11
AEMeasurable.evalproof · cited by 7
ProbabilityTheory.BrownianReal.covariance_eval_projectiveFamilyproof · cited by 4

Results whose statement or proof uses this declaration.