tendsto mixing nat and int

Stream: maths

[Filippo A. E. Nuccio]

Do we have the following

example (f : ℤ → ℝ) (d : ℤ) (a : ℝ) : tendsto (λ n : ℕ, f n) at_top (𝓝 a) ↔
  tendsto (λ n : ℕ, f (n + d)) at_top (𝓝 a) :=

(if you replace all ℤ by ℕ in the above example, this is exactly docs#filter.tendsto_add_at_top_iff_nat). This would be immediate to prove if (λ n : ℕ, f (n + d)) sent the at_top filter of ℕ to itself, which is true but I cannot say it: I tried

lemma map_zadd_at_top_eq_nat (d : ℤ) : map (λ a : ℕ, a + d) (at_top : filter ℕ) = (at_top : filter ℕ) :=

but of course got the error that the map (λ n : ℕ, f (n + d)) does not respect ℕ. I would have an idea on how to prove the lemma using some "eventual" business, but I do not actually know how to state it...

[Adam Topaz]

There must be some way, using filter voodoo, of using the fact that these two maps are eventually the same, where eventually is in the sense of the filters involved. But I also don't immediately see how to formulate the statement!

[Filippo A. E. Nuccio]

Yes, I also see the proof of a statement I can't state... :cold_sweat:

[Adam Topaz]

@Filippo A. E. Nuccio can you give me your imports?

[Filippo A. E. Nuccio]

import data.int.interval
import data.finset.nat_antidiagonal
import laurent_measures.basic
import laurent_measures.theta
import linear_algebra.basic

[Adam Topaz]

Mathlib only imports?

[Filippo A. E. Nuccio]

Ah, how can I get this? Should I retrace back all the mathlib imports in those files, or is there a way to ask Lean about this?

[Adam Topaz]

It's okay, I can probably figure it out.

[Adam Topaz]

A not-so-minimal import list, in case it helps anyone else:

import data.int.interval
import data.finset.nat_antidiagonal
import linear_algebra.basic
import analysis.special_functions.pow
import analysis.special_functions.log
import analysis.specific_limits
import category_theory.Fintype
import analysis.normed_space.basic

[Filippo A. E. Nuccio]

(I don't think I need the category_theory.Fintype for the statement at hand)

[Patrick Massot]

I can have a look if you want

[Filippo A. E. Nuccio]

Thanks!

[Patrick Massot]

I proved it by brute forcing a lemma for Filippo:

import order.filter.at_top_bot tactic.linarith

open filter

lemma filippo : map (coe : ℕ → ℤ) at_top = at_top :=
begin
  ext s,
  simp only [set.mem_preimage, mem_at_top_sets, ge_iff_le, mem_map],
  split,
  { rintro ⟨a, ha⟩,
    use a,
    intros b hb,
    lift b to ℕ,
    apply ha,
    exact_mod_cast hb,
    linarith },
  { rintro ⟨a, ha⟩,
    use a.nat_abs,
    intros b hb,
    apply ha,
    apply int.le_nat_abs.trans,
    exact_mod_cast hb }
end

example {X : Type*} {f : ℤ → X} (F : filter X) : tendsto (λ n : ℕ, f n) at_top F ↔
  tendsto f at_top F :=
show map (f ∘ coe) _ ≤ _ ↔ _, by simpa [← map_map, filippo]

[Patrick Massot]

The first proof is ugly because I didn't took time to think about the proper generality so I proved it by brute force. But then the example becomes obvious

[Filippo A. E. Nuccio]

Thanks!

[Filippo A. E. Nuccio]

I'll have a look and ask if I have questions (in the meanwhile, I will also copy-paste it in LTE, with your permission :smile: )

[Patrick Massot]

Sure.

[Filippo A. E. Nuccio]

Thanks!

[Anatole Dedecker]

See docs#tendsto_coe_nat_at_top_at_top