isLittleO_one_left_iff — Mathlib

English

IsLittleO with constant-one left characterizes tendsto to zero of f.

Русский

IsLittleO слева с константой единицы характеризует стремление f к нулю.

LaTeX

$$isLittleO_one_left_iff$$

Lean4

@[simp]
theorem isLittleO_one_left_iff : (fun _x => 1 : α → F) =o[l] f ↔ Tendsto (fun x => ‖f x‖) l atTop :=
  calc
    (fun _x => 1 : α → F) =o[l] f ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖(1 : F)‖ ≤ ‖f x‖ :=
      isLittleO_iff_nat_mul_le_aux <| Or.inl fun _x => by simp only [norm_one, zero_le_one]
    _ ↔ ∀ n : ℕ, True → ∀ᶠ x in l, ‖f x‖ ∈ Ici (n : ℝ) := by simp only [norm_one, mul_one, true_imp_iff, mem_Ici]
    _ ↔ Tendsto (fun x => ‖f x‖) l atTop := atTop_hasCountableBasis_of_archimedean.1.tendsto_right_iff.symm

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