English
For L1, L2 in StrongDual ℝ E, the operator norm of the uncentered covariance dual is bounded by the product of the operator norms of L1 and L2 times the μ-second moment of the space: ‖uncenteredCovarianceBilinDual μ L1 L2‖ ≤ ‖L1‖ ‖L2‖ ∫ ‖x‖^2 dμ.
Русский
Для L1, L2 в StrongDual ℝ E нормa оператора нецентрированной ковариационной двойной формы удовлетворяет: ‖uncenteredCovarianceBilinDual μ L1 L2‖ ≤ ‖L1‖ ‖L2‖ ∫ ‖x‖^2 dμ.
LaTeX
$$$\\|\\operatorname{uncenteredCovarianceBilinDual}(\\mu)(L_1,L_2)\\| \\leq \\|L_1\\| \\|L_2\\| \\int_E \\|x\\|^2 \\, d\\mu(x)$$$
Lean4
theorem norm_uncenteredCovarianceBilinDual_le (L₁ L₂ : StrongDual ℝ E) :
‖uncenteredCovarianceBilinDual μ L₁ L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ :=
by
by_cases h : MemLp id 2 μ
swap; · simp only [uncenteredCovarianceBilinDual_of_not_memLp h, norm_zero]; positivity
calc
‖uncenteredCovarianceBilinDual μ L₁ L₂‖
_ = ‖∫ x, L₁ x * L₂ x ∂μ‖ := by rw [uncenteredCovarianceBilinDual_apply h]
_ ≤ ∫ x, ‖L₁ x‖ * ‖L₂ x‖ ∂μ := ((norm_integral_le_integral_norm _).trans (by simp))
_ ≤ ∫ x, ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ :=
by
refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
· simp_rw [← norm_mul]
exact (MemLp.integrable_mul (h.continuousLinearMap_comp L₁) (h.continuousLinearMap_comp L₂)).norm
· simp_rw [mul_assoc]
refine Integrable.const_mul ?_ _
simp_rw [← mul_assoc, mul_comm _ (‖L₂‖), mul_assoc, ← pow_two]
refine Integrable.const_mul ?_ _
exact h.integrable_norm_pow (by simp)
· simp only
rw [mul_assoc]
gcongr
· exact ContinuousLinearMap.le_opNorm L₁ x
· exact ContinuousLinearMap.le_opNorm L₂ x
_ = ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ := by
rw [← integral_const_mul]
congr with x
ring
