integrable_exp_mul_of_nonneg_of_le

English

Under MemLp id 2 μ, the covariance bilinear dual satisfies covarianceBilinDual μ L1 L2 = ∫ (L1(x) - μ[L1])(L2(x) - μ[L2]) dμ.

Русский

При MemLp id 2 μ ковариационная билинейная двойка удовлетворяет covarianceBilinDual μ L1 L2 = ∫ (L1(x) - μ[L1])(L2(x) - μ[L2]) dμ.

LaTeX

$$$covarianceBilinDual(\\mu) L_1 L_2 = \\int_E (L_1(x) - \\mu[L_1])(L_2(x) - \\mu[L_2]) \\, d\\mu(x)$$$

Lean4

/-- If `ω ↦ exp (u * X ω)` is integrable at `u ≥ 0`, then it is integrable on `[0, u]`. -/
theorem integrable_exp_mul_of_nonneg_of_le [IsFiniteMeasure μ] (hu : Integrable (fun ω ↦ exp (u * X ω)) μ)
    (h_nonneg : 0 ≤ t) (htu : t ≤ u) : Integrable (fun ω ↦ exp (t * X ω)) μ :=
  integrable_exp_mul_of_le_of_le (by simp) hu h_nonneg htu

Похожие утверждения