English
If f is strongly measurable and f(x) is a.e. bounded by c, then almost everywhere Tendsto of approxBounded holds.
Русский
Если f сильно измерима и почти всюду ограничена верхней Bound, тогда почти во всех точках выполняется Tendsto от ограниченного приближенного диапазона.
LaTeX
$$If hf is strongly measurable and hf_bound holds a.e., then ∀ᵐ x, Tendsto (hf.approxBounded c n x) atTop (f x)$$
Lean4
theorem tendsto_approxBounded_of_norm_le {β} {f : α → β} [NormedAddCommGroup β] [NormedSpace ℝ β]
{m : MeasurableSpace α} (hf : StronglyMeasurable[m] f) {c : ℝ} {x : α} (hfx : ‖f x‖ ≤ c) :
Tendsto (fun n => hf.approxBounded c n x) atTop (𝓝 (f x)) :=
by
have h_tendsto := hf.tendsto_approx x
simp only [StronglyMeasurable.approxBounded, SimpleFunc.coe_map, Function.comp_apply]
by_cases hfx0 : ‖f x‖ = 0
· rw [norm_eq_zero] at hfx0
rw [hfx0] at h_tendsto ⊢
have h_tendsto_norm : Tendsto (fun n => ‖hf.approx n x‖) atTop (𝓝 0) :=
by
convert h_tendsto.norm
rw [norm_zero]
refine squeeze_zero_norm (fun n => ?_) h_tendsto_norm
calc
‖min 1 (c / ‖hf.approx n x‖) • hf.approx n x‖ = ‖min 1 (c / ‖hf.approx n x‖)‖ * ‖hf.approx n x‖ := norm_smul _ _
_ ≤ ‖(1 : ℝ)‖ * ‖hf.approx n x‖ :=
by
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
rw [norm_one, Real.norm_of_nonneg]
· exact min_le_left _ _
· exact le_min zero_le_one (div_nonneg ((norm_nonneg _).trans hfx) (norm_nonneg _))
_ = ‖hf.approx n x‖ := by rw [norm_one, one_mul]
rw [← one_smul ℝ (f x)]
refine Tendsto.smul ?_ h_tendsto
have : min 1 (c / ‖f x‖) = 1 :=
by
rw [min_eq_left_iff, one_le_div (lt_of_le_of_ne (norm_nonneg _) (Ne.symm hfx0))]
exact hfx
nth_rw 2 [this.symm]
refine Tendsto.min tendsto_const_nhds ?_
exact Tendsto.div tendsto_const_nhds h_tendsto.norm hfx0
