English
Take normed groups K and R, with a bilinear action of K on R. If the product ‖f(x) • g(x)‖ stays bounded along a filter l and f(x) tends to infinity (cobounded) in K, then g(x) tends to 0 in R along l.
Русский
Для нормированных групп K и R с билинейным действием, если ‖f(x) • g(x)‖ ограничено вдоль фильтра l и f(x) становится бесконечно большим в K, то g(x) стремится к нулю в R вдоль l.
LaTeX
$$$\text{IsBoundedUnder}(\le, l, x \mapsto \|f(x) \cdot g(x)\|) \;\land\; f \to_{l} \text{cobounded}(K) \Rightarrow g \to_{l} 0$$$
Lean4
theorem tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded [NormedAddGroup K] [NormedAddGroup R]
[SMulWithZero K R] [NoZeroSMulDivisors K R] [NormSMulClass K R] {f : α → K} {g : α → R} {l : Filter α}
(hmul : IsBoundedUnder (· ≤ ·) l fun x ↦ ‖f x • g x‖) (hf : Tendsto f l (cobounded K)) : Tendsto g l (𝓝 0) :=
by
obtain ⟨c, hc⟩ := hmul.eventually_le
refine Metric.nhds_basis_closedBall.tendsto_right_iff.mpr fun ε hε0 ↦ ?_
filter_upwards [hc, hasBasis_cobounded_norm.tendsto_right_iff.mp hf (c / ε) trivial,
hf.eventually_ne_cobounded 0] with x hfgc hεf hf0
rcases eq_or_lt_of_le ((norm_nonneg _).trans hfgc) with rfl | hc0
· simpa [(smul_eq_zero_iff_right hf0).mp (norm_le_zero_iff.mp hfgc)] using hε0.le
calc
_ = ‖g x‖ := by simp
_ ≤ c / ‖f x‖ := by rwa [norm_smul, ← le_div_iff₀' (by positivity)] at hfgc
_ ≤ c / (c / ε) := by gcongr
_ = ε := div_div_cancel₀ hc0.ne'
