English
For L1, L2 in StrongDual ℝ E and MemLp id 2 μ, the norm of the covariance is bounded by ‖L1‖‖L2‖ ∫ ‖x‖^2 dμ.
Русский
Для L1, L2 в StrongDual ℝ E и MemLp id 2 μ нормa ковариации удовлетворяет: ‖covarianceBilinDual μ L1 L2‖ ≤ ‖L1‖‖L2‖ ∫ ‖x‖^2 dμ.
LaTeX
$$$\\|uncenteredCovarianceBilinDual(\\mu)(L_1,L_2)\\| \\leq \\|L_1\\| \\|L_2\\| \\int_E \\|x\\|^2 \\, d\\mu(x)$$$
Lean4
theorem integrable_exp_mul_of_le_of_le {a b : ℝ} (ha : Integrable (fun ω ↦ exp (a * X ω)) μ)
(hb : Integrable (fun ω ↦ exp (b * X ω)) μ) (hat : a ≤ t) (htb : t ≤ b) : Integrable (fun ω ↦ exp (t * X ω)) μ :=
by
refine Integrable.mono (ha.add hb) ?_ (ae_of_all _ fun ω ↦ ?_)
· by_cases hab : a = b
· have ha_eq_t : a = t := le_antisymm hat (hab ▸ htb)
rw [← ha_eq_t]
exact ha.1
· refine AEMeasurable.aestronglyMeasurable ?_
refine measurable_exp.comp_aemeasurable (AEMeasurable.const_mul ?_ _)
by_cases ha_zero : a = 0
· refine aemeasurable_of_aemeasurable_exp_mul ?_ hb.1.aemeasurable
rw [ha_zero] at hab
exact Ne.symm hab
· exact aemeasurable_of_aemeasurable_exp_mul ha_zero ha.1.aemeasurable
· simp only [norm_eq_abs, abs_exp, Pi.add_apply]
conv_rhs => rw [abs_of_nonneg (by positivity)]
rcases le_total 0 (X ω) with h | h
·
calc
exp (t * X ω)
_ ≤ exp (b * X ω) := (exp_le_exp.mpr (mul_le_mul_of_nonneg_right htb h))
_ ≤ exp (a * X ω) + exp (b * X ω) := le_add_of_nonneg_left (exp_nonneg _)
·
calc
exp (t * X ω)
_ ≤ exp (a * X ω) := (exp_le_exp.mpr (mul_le_mul_of_nonpos_right hat h))
_ ≤ exp (a * X ω) + exp (b * X ω) := le_add_of_nonneg_right (exp_nonneg _)
