isBoundedAt_iff — Mathlib

English

Let c be a cusp and f a function with weight k. If g maps ∞ to c, then f is bounded at c with weight k iff f|[k]g is bounded at ∞.

Русский

Пусть c — вершина ( cusp ), и f — функция с весом k. Если g переводит ∞ в c, то f ограничена в c с весом k тогда и только тогда, когда f|[k]g ограничена в ∞.

LaTeX

$$$\mathrm{IsBoundedAt}(c,f,k) \iff \mathrm{IsBoundedAtImInfty}(f \lvert[k] g)$ при условии $g\cdot \infty = c$$$

Lean4

/-- To check that `f` is bounded at `c`, it suffices for `f ∣[k] g` to be bounded at `∞` for any
single `g` with `g • ∞ = c`. -/
theorem isBoundedAt_iff (hg : g • ∞ = c) : IsBoundedAt c f k ↔ IsBoundedAtImInfty (f ∣[k] g) :=
  ⟨fun hc ↦ hc g hg, by simp [← hg, IsBoundedAt.smul_iff, isBoundedAt_infty_iff]⟩

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