tendsto_indicator_ge — Mathlib

English

For a fixed x, as M grows, the indicator of the set {x | M ≤ ||f(x)||_+} applied to f tends to 0 in the target topology.

Русский

Для фиксированного x, при росте M индикатор множества {x | M ≤ ||f(x)||_+} в применении к f стремится к нулю в целевом топологическом пространстве.

LaTeX

$$$ \\text{Tendsto} (M \\mapsto \\mathbf{1}_{\\{x : M \\le \\|f(x)\\|_+\\}}(f(x)))_{M \\to \\infty} \\to 0 $$$

Lean4

theorem tendsto_indicator_ge (f : α → β) (x : α) :
    Tendsto (fun M : ℕ => {x | (M : ℝ) ≤ ‖f x‖₊}.indicator f x) atTop (𝓝 0) :=
  by
  refine tendsto_atTop_of_eventually_const (i₀ := Nat.ceil (‖f x‖₊ : ℝ) + 1) fun n hn => ?_
  rw [Set.indicator_of_notMem]
  simp only [not_le, Set.mem_setOf_eq]
  refine lt_of_le_of_lt (Nat.le_ceil _) ?_
  refine lt_of_lt_of_le (lt_add_one _) ?_
  norm_cast

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