English
If f tends to 1 and g is bounded, and op has a growth bound, then the combination op(f,g) tends to 1.
Русский
Если f стремится к 1 и g ограничено, и операция op удовлетворяет ограничению роста, то сумма/произведение op(f,g) стремится к 1.
LaTeX
$$Tendsto (fun x => op (f x) (g x)) l (nhds 1)$$
Lean4
/-- A helper lemma used to prove that the (scalar or usual) product of a function that tends to one
and a bounded function tends to one. This lemma is formulated for any binary operation
`op : E → F → G` with an estimate `‖op x y‖ ≤ A * ‖x‖ * ‖y‖` for some constant A instead of
multiplication so that it can be applied to `(*)`, `flip (*)`, `(•)`, and `flip (•)`. -/
@[to_additive /-- A helper lemma used to prove that the (scalar or usual) product of a function that
tends to zero and a bounded function tends to zero. This lemma is formulated for any binary
operation `op : E → F → G` with an estimate `‖op x y‖ ≤ A * ‖x‖ * ‖y‖` for some constant A instead
of multiplication so that it can be applied to `(*)`, `flip (*)`, `(•)`, and `flip (•)`. -/
]
theorem op_one_isBoundedUnder_le' {f : α → E} {g : α → F} {l : Filter α} (hf : Tendsto f l (𝓝 1))
(hg : IsBoundedUnder (· ≤ ·) l (Norm.norm ∘ g)) (op : E → F → G) (h_op : ∃ A, ∀ x y, ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) :
Tendsto (fun x => op (f x) (g x)) l (𝓝 1) :=
by
obtain ⟨A, h_op⟩ := h_op
rcases hg with ⟨C, hC⟩; rw [eventually_map] at hC
rw [NormedCommGroup.tendsto_nhds_one] at hf ⊢
intro ε ε₀
rcases exists_pos_mul_lt ε₀ (A * C) with ⟨δ, δ₀, hδ⟩
filter_upwards [hf δ δ₀, hC] with i hf hg
refine (h_op _ _).trans_lt ?_
rcases le_total A 0 with hA | hA
·
exact
(mul_nonpos_of_nonpos_of_nonneg (mul_nonpos_of_nonpos_of_nonneg hA <| norm_nonneg' _) <| norm_nonneg' _).trans_lt
ε₀
calc
A * ‖f i‖ * ‖g i‖ ≤ A * δ * C := by gcongr; exact hg
_ = A * C * δ := (mul_right_comm _ _ _)
_ < ε := hδ
