ae_enorm_le_bound — Mathlib

English

If bound' has finite integral and F'n are pointwise dominated by bound' and converge to f', then HasFiniteIntegral f' μ.

Русский

Если bound' имеет конечный интеграл и F'n доминируются bound' и сходятся к f' почти всюду, то HasFiniteIntegral f' μ.

LaTeX

$$$HasFiniteIntegral bound' μ \Rightarrow (\forall n, \forallᵐ a, \|F'n a\| ≤ bound' a) \land (\forallᵐ a, Tendsto (F'n a) atTop (nhds f' a)) \Rightarrow HasFiniteIntegral f' μ$$$

Lean4

theorem ae_enorm_le_bound (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F' n a‖ₑ ≤ bound' a)
    (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))) : ∀ᵐ a ∂μ, ‖f' a‖ₑ ≤ bound' a :=
  by
  rw [← ae_all_iff] at h_bound
  apply h_bound.mp ((ae_tendsto_enorm h_lim).mono _)
  intro a tendsto_norm h_bound
  exact le_of_tendsto' tendsto_norm h_bound

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