isBigO_one_nhds_ne_iff — Mathlib

English

IsBigO with nhds top is equivalent to a supremum norm bound over the entire space.

Русский

IsBigO с nhds сверху эквивалентно верхней границе нормы по всему пространству.

LaTeX

$$isBigO_top$$

Lean4

/-- The condition `f = O[𝓝[≠] a] 1` is equivalent to `f = O[𝓝 a] 1`. -/
theorem isBigO_one_nhds_ne_iff [TopologicalSpace α] {a : α} :
    f =O[𝓝[≠] a] (fun _ ↦ 1 : α → F) ↔ f =O[𝓝 a] (fun _ ↦ 1 : α → F) :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ h.mono nhdsWithin_le_nhds⟩
  simp only [isBigO_one_iff, IsBoundedUnder, IsBounded, eventually_map] at h ⊢
  obtain ⟨c, hc⟩ := h
  use max c ‖f a‖
  filter_upwards [eventually_nhdsWithin_iff.mp hc] with b hb
  rcases eq_or_ne b a with rfl | hb'
  · apply le_max_right
  · exact (hb hb').trans (le_max_left ..)

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