limUnder_add_atTop_eq_nat

Stream: new members

[Arshak Parsa]

Is this theorem provable?

import Mathlib

theorem limUnder_add_atTop_eq_nat
  [TopologicalSpace α] [Nonempty α]
  (f : ℕ → α) (k : ℕ) :
    limUnder atTop (fun n => f (n + k)) = limUnder atTop (fun n => f n) := by
  sorry

this is OK when the limit exists, but what happens if the limit does not exist?

[Kevin Buzzard]

It's not obviously OK when the limit exists, as in this generality a sequence can have more than one limit, so how can you be sure that the two limUnders are choosing the same one?

However if you unfold the definitions it looks to me like probably this result is provable. Start with

import Mathlib

set_option autoImplicit true

theorem limUnder_add_atTop_eq_nat
  [TopologicalSpace α] [Nonempty α]
  (f : ℕ → α) (k : ℕ) :
    limUnder atTop (fun n => f (n + k)) = limUnder atTop (fun n => f n) := by
  refine congr_arg Classical.epsilon ?h
  ext x
  -- looks OK

and now it looks like you have to prove that the set of limit points is the same for both f and shifted-f, which should be OK.

[Arshak Parsa]

tendsto_add_atTop_iff_nat is true, but I'm not sure what happens if the limit does not exist.

[Vincent Beffara]

Then neither limit exists and presumably you get the same junk value on both sides so equality still holds

[Vincent Beffara]

Also, check docs#Filter.map_add_atTop_eq_nat

[Vincent Beffara]

import Mathlib

theorem limUnder_add_atTop_eq_nat
  [TopologicalSpace α] [Nonempty α]
  (f : ℕ → α) (k : ℕ) :
    limUnder Filter.atTop (fun n => f (n + k)) = limUnder Filter.atTop (fun n => f n) := by
  unfold limUnder
  change lim (Filter.map (f ∘ fun n => (n + k)) _) = _
  rw [← Filter.map_compose]
  change lim (Filter.map f (Filter.map (fun n => n + k) _)) = _
  rw [Filter.map_add_atTop_eq_nat k]

[Vincent Beffara]

Note that your initial statement is not provable because AtTop (rather than Filter.AtTop) is taken as an implicit parameter, so you are stating that it holds for any filter, which it doen't.

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

Here's my effort:

import Mathlib

variable (α : Type)
 open Filter

theorem limUnder_add_atTop_eq_nat
  [TopologicalSpace α] [Nonempty α]
  (f : ℕ → α) (k : ℕ) :
    limUnder atTop (fun n => f (n + k)) = limUnder atTop (fun n => f n) := by
  refine congr_arg Classical.epsilon ?h
  ext x
  change map (f ∘ fun n ↦ n + k) _ ≤ _ ↔ _
  rw [← map_compose]
  unfold Function.comp
  rw [map_add_atTop_eq_nat]