English
For L1, L2 in StrongDual Real E, the norm of covarianceBilinDual μ L1 L2 is bounded by the product of operator norms times ∫ ‖x‖^2 dμ.
Русский
Для L1, L2 в StrongDual Real E норма covarianceBilinDual μ L1 L2 ограничена произведением норм операторов и интегралом ‖x‖^2 dμ.
LaTeX
$$$\\|covarianceBilinDual(\\mu)(L_1,L_2)\\| ≤ \\|L_1\\| \\|L_2\\| \\int_E \\|x\\|^2 \\, d\\mu(x)$$$
Lean4
/-- If `ω ↦ exp (u * X ω)` is integrable at `u` and `-u`, then it is integrable on `[-u, u]`. -/
theorem integrable_exp_mul_of_abs_le (hu_int_pos : Integrable (fun ω ↦ exp (u * X ω)) μ)
(hu_int_neg : Integrable (fun ω ↦ exp (-u * X ω)) μ) (htu : |t| ≤ |u|) : Integrable (fun ω ↦ exp (t * X ω)) μ :=
by
refine integrable_exp_mul_of_le_of_le (a := -|u|) (b := |u|) ?_ ?_ ?_ ?_
· rcases le_total 0 u with hu | hu
· rwa [abs_of_nonneg hu]
· simpa [abs_of_nonpos hu]
· rcases le_total 0 u with hu | hu
· rwa [abs_of_nonneg hu]
· rwa [abs_of_nonpos hu]
· rw [neg_le]
exact (neg_le_abs t).trans htu
· exact (le_abs_self t).trans htu
