Theorems · Definition · probability

ProbabilityTheory.covarianceBilinDual

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

Continuous bilinear form with value ∫ x, (L₁ x - μ[L₁]) * (L₂ x - μ[L₂]) ∂μ on (L₁, L₂) if MemLp id 2 μ. If not, we set it to zero.

Defined in

Mathlib.Probability.Moments.CovarianceBilinDual

Cited by

22 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceBorelSpace