tendsto_approxBounded_ae — Mathlib

English

For any strongly measurable f and c≥0, the norm of the bounded approximation is always ≤ c.

Русский

Для любого сильно измеримого f и c≥0, норма ограниченного приближения не превосходит c.

LaTeX

$$$\\|hf.approxBounded c n x\\| ≤ c$$$

Lean4

theorem tendsto_approxBounded_ae {β} {f : α → β} [NormedAddCommGroup β] [NormedSpace ℝ β] {m m0 : MeasurableSpace α}
    {μ : Measure α} (hf : StronglyMeasurable[m] f) {c : ℝ} (hf_bound : ∀ᵐ x ∂μ, ‖f x‖ ≤ c) :
    ∀ᵐ x ∂μ, Tendsto (fun n => hf.approxBounded c n x) atTop (𝓝 (f x)) := by
  filter_upwards [hf_bound] with x hfx using tendsto_approxBounded_of_norm_le hf hfx

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