Documentation

BrownianMotion.Gaussian.CovarianceBilin

Covariance bilinear form #

theorem ProbabilityTheory.covarianceBilin_apply' {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [NormedSpace E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (L₁ L₂ : NormedSpace.Dual E) :
((covarianceBilin μ) L₁) L₂ = (x : E), L₁ (x - (x : E), id x μ) * L₂ (x - (x : E), id x μ) μ