English
Let μ be a measure on a normed space E and L1, L2 be elements of the real dual space. If L1 and L2 are 2-integrable with respect to μ via the identity map (MemLp id 2 μ), then the uncentered covariance bilinear dual evaluated at μ, L1, L2 equals the integral of the product L1(x) L2(x) with respect to μ: ∫ L1(x) L2(x) dμ.
Русский
Пусть μ — мера на нормированном пространстве E, а L1, L2 — элементы двойственного пространства Real. Если L1 и L2 являются 2-интегрируемыми по μ через тождественную карту (MemLp id 2 μ), то нецентрированная ковариантная билинейная форма равна интегралу произведения L1(x) и L2(x) по μ: ∫ L1(x) L2(x) dμ.
LaTeX
$$$\\operatorname{uncenteredCovarianceBilinDual}(\\mu)(L_1,L_2) = \\int_E L_1(x) L_2(x) \\, d\\mu(x)$$$
Lean4
theorem uncenteredCovarianceBilinDual_apply (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
uncenteredCovarianceBilinDual μ L₁ L₂ = ∫ x, L₁ x * L₂ x ∂μ :=
by
simp only [uncenteredCovarianceBilinDual, ContinuousLinearMap.bilinearComp_apply, StrongDual.toLp_apply h,
L2.inner_def, RCLike.inner_apply, conj_trivial]
refine integral_congr_ae ?_
filter_upwards [MemLp.coeFn_toLp (h.continuousLinearMap_comp L₁),
MemLp.coeFn_toLp (h.continuousLinearMap_comp L₂)] with x hxL₁ hxL₂
simp only [id_eq] at hxL₁ hxL₂
rw [hxL₁, hxL₂, mul_comm]
