Zulip Chat Archive

Stream: maths

Topic: names?


view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 02:30):

Hi, what would be a good name for the following lemmas?

lemma TODO1 {α β : Type*} [semilattice_sup β] [nonempty β]
  {l : filter α} (hl : has_countable_basis l)
  {x :   β  α} (hx :  s  l,  k n in at_top, x k n  s) :
   (N :   β) in at_top, tendsto (λ k, x k (N k)) at_top l := sorry

lemma TODO2 {α : Type*} [topological_space α] [first_countable_topology α]
  {x :     α} {y :   α} {z : α}
  (hx :  k in at_top, tendsto (x k) at_top (𝓝 (y k))) (hy : tendsto y at_top (𝓝 z)) :
   (N :   ) in at_top, tendsto (λ k, x k (N k)) at_top (𝓝 z) := sorry

lemma TODO3 {α : Type*} {l : filter α} (hl : has_countable_basis l)
  {x :     α} (hx :  k in at_top, tendsto (x k) at_top l) :
   (N :   ) in at_top, tendsto (λ k, x k (N k)) at_top l := sorry

The main lemma TODO1 and its particular cases TODO2 and TODO3 formalize the following common practice. Consider a sequence of sequences x : ℕ → ℕ → α. Suppose that each x k has a limit y k (either finite or infinite), and these limits converge to z. Then x k (n k) tends to z provided that n k tends to infinity sufficiently fast.

view this post on Zulip Sebastien Gouezel (Feb 10 2020 at 08:19):

tendsto_of_tendsto_of_tendsto_of_sufficiently_fast_growth for the second one?

I didn't know that ∀ᶠ (N : ℕ → β) in at_top makes sense, i.e., that there is an at_top filter on ℕ → β. I think these lemmas will need ample docstrings to explain what is going on :)


Last updated: May 06 2021 at 19:30 UTC