English
The covariance bilinear dual is the continuous bilinear form on StrongDual Real E given by uncentered covariance after centering with respect to μ, i.e., centered by μ[L], if memLp holds; otherwise it is the zero form.
Русский
Ковариационная билинейная двойка — непрерывная билинейная форма на StrongDual Real E, заданная нецентрированной ковариацией после центрирования по μ, то есть по μ[L], если выполняется memLp; иначе — нулевая форма.
LaTeX
$$$covarianceBilinDual(\\mu) = uncenteredCovarianceBilinDual\\bigl(\\mu \\mapsto (x \\mapsto x - \\mu[x])\\bigr)$$$
Lean4
/-- 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. -/
noncomputable def covarianceBilinDual (μ : Measure E) : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
uncenteredCovarianceBilinDual (μ.map (fun x ↦ x - ∫ x, x ∂μ))
