Theorems · Definition · probability

ProbabilityTheory.uncenteredCovarianceBilinDual

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {mE : MeasurableSpace E} →
      [inst_1 : NormedSpace ℝ E] →
        [OpensMeasurableSpace E] → MeasureTheory.Measure E → StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ

Continuous bilinear form with value ∫ x, L₁ x * L₂ x ∂μ on (L₁, L₂). This is equal to the covariance only if μ is centered.

Defined in

Mathlib.Probability.Moments.CovarianceBilinDual

Cited by

10 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceOpensMeasurableSpace