all_ae_ofReal_f_le_bound — Mathlib

English

If f: α → β has finite integral, then for any constant c, HasFiniteIntegral (fun x => c · f x) μ.

Русский

Если f: α → β имеет конечный интеграл, то для любого фиксированного c имеет место HasFiniteIntegral (c · f) μ.

LaTeX

$$$HasFiniteIntegral f μ \Rightarrow \forall c, HasFiniteIntegral (x \mapsto c \cdot f x) μ$$$

Lean4

theorem all_ae_ofReal_f_le_bound (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a)
    (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))) :
    ∀ᵐ a ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a) :=
  by
  have F_le_bound := all_ae_ofReal_F_le_bound h_bound
  rw [← ae_all_iff] at F_le_bound
  apply F_le_bound.mp ((all_ae_tendsto_ofReal_norm h_lim).mono _)
  intro a tendsto_norm F_le_bound
  exact le_of_tendsto' tendsto_norm F_le_bound

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