integrable_mulExpNegMulSq_comp — Mathlib

English

If f ∈ C(E, ℝ) and ε > 0, then ∫ mulExpNegMulSq ε (f) dP is finite (i.e., the composite is integrable).

Русский

Если f ∈ C(E, ℝ) и ε > 0, то интеграл ∫ mulExpNegMulSq ε (f) dP конечен.

LaTeX

$$$\\forall f:\\u00A0C(E, \\mathbb{R}),\\; \\varepsilon>0\\;\\Rightarrow\\; \\int_E mulExpNegMulSq(\\varepsilon, f(x))\\, dP < \\infty$$$

Lean4

theorem integrable_mulExpNegMulSq_comp (f : C(E, ℝ)) (hε : 0 < ε) : Integrable (fun x => mulExpNegMulSq ε (f x)) P :=
  by
  apply integrable P ⟨⟨fun x => mulExpNegMulSq ε (f x), by fun_prop⟩, ⟨2 * (√ε)⁻¹, _⟩⟩
  exact fun x y => dist_mulExpNegMulSq_le_two_mul_sqrt hε (f x) (f y)

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