Theorems · Definition · probability

ProbabilityTheory.covarianceBilin

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [inst_2 : MeasurableSpace E] → [BorelSpace E] → MeasureTheory.Measure E → E →L[ℝ] E →L[ℝ] ℝ

Covariance of a measure on an inner product space, as a continuous bilinear form.

Defined in

Mathlib.Probability.Moments.CovarianceBilin

Cited by

25 results in Mathlib

Foundations

Depth 270 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpace