Moving to the limit in equalities

Stream: Is there code for X?

[Ryan Lahfa]

Hello there,
I'm looking for general techniques in mathlib for things such as:

Let be $f, g: \mathbb{R} \to \mathbb{R}$ such that $\lim_{+\infty} g$ and $\lim_{+\infty} f/(1 - g)$ exist.
I would like to prove that $\lim_{+\infty} f$ exist (and its value is what should be expected).

I can see theorems to prove composition of limits (filter.tendsto.comp), but it seems like I would need something to inverse the second limit hypothesis.
I am also trying to avoid as much as possible epsilon-delta definitions to maximally reuse filter theory, but these theorems looks very epsilon-delta IMHO.

Precisely, I am looking for proofs of things like that:

import analysis.specific_limits

lemma tendsto_aux1 {l: ℝ} {f g: ℝ → ℝ}
  (hg: filter.tendsto g filter.at_top (nhds 0))
  (hc: filter.tendsto (f / (1 - g)) filter.at_top (nhds l)):
  filter.tendsto f filter.at_top (nhds l) := sorry

[Patrick Massot]

This lemma is false.

[Patrick Massot]

So you need to switch to another proof assistant to prove it (I hear that Agda should work nicely here).

[Ryan Lahfa]

Patrick Massot said:

This lemma is false.

I was pretty sure I was going to write something false :>

[Eric Wieser]

How easy is the proof that it's false? Is it within the grasp of docs#tactic.interactive.slim_check?

[Patrick Massot]

I don't think slim_check would be a natural fit here.

[Patrick Massot]

It could easily instantiate the lemma with data that makes it wrong, but I fear we couldn't check the conclusion.

[Ryan Lahfa]

So assuming l is not a filter \R but some nhds of a finite value, I believe (quick proof sketching seems to confirm) it is true.

[Reid Barton]

Is the lemma really false? Note that it doesn't say the same thing as the math summary beforehand (even ignoring the issue which I think you're referring to).

[Reid Barton]

oh I didn't notice l was an arbitrary filter

[Ryan Lahfa]

Maybe, a good start would be also something like this:

lemma tendsto_aux2 {l: ℝ} {f g: ℝ → ℝ}
  (hfg: filter.tendsto (f - g) filter.at_top (nhds 0))
  (hg: filter.tendsto g filter.at_top (nhds l)):
  filter.tendsto f filter.at_top (nhds l) := sorry

[Patrick Massot]

Ryan Lahfa said:

So assuming l is not a filter \R but some nhds of a finite value, I believe (quick proof sketching seems to confirm) it is true.

import analysis.specific_limits

open filter
open_locale topological_space filter

lemma tendsto_aux1 {l: ℝ} {f g: ℝ → ℝ}
  (hg: tendsto g at_top (𝓝  0))
  (hc: tendsto (f / (1 - g)) at_top (𝓝 l)):
  tendsto f at_top (𝓝 l) :=
begin
  have lim₁ : tendsto (1 - g) at_top (𝓝 1),
  { rw ← sub_zero (1 : ℝ),
    exact tendsto_const_nhds.sub hg },
  have : (λ (x : ℝ), (1 - g) x * (f / (1 - g)) x) =ᶠ[at_top] f,
  { have : {(0 : ℝ)}ᶜ ∈ 𝓝 (1 : ℝ) := compl_singleton_mem_nhds zero_ne_one.symm,
    have : ∀ᶠ (x : ℝ) in at_top, (1 - g) x ∈ ({(0 : ℝ)} : set ℝ)ᶜ := lim₁ this,
    apply this.mono,
    intros x hx,
    replace hx : 1 - g x ≠ 0, by simpa using hx,
    exact mul_div_cancel' _ hx  },
  simpa using (tendsto_congr' this).mp (lim₁.mul hc)
end

[Ryan Lahfa]

Patrick Massot said:

Ryan Lahfa said:

So assuming l is not a filter \R but some nhds of a finite value, I believe (quick proof sketching seems to confirm) it is true.

import analysis.specific_limits

open filter
open_locale topological_space filter

lemma tendsto_aux1 {l: ℝ} {f g: ℝ → ℝ}
  (hg: tendsto g at_top (𝓝  0))
  (hc: tendsto (f / (1 - g)) at_top (𝓝 l)):
  tendsto f at_top (𝓝 l) :=
begin
  have lim₁ : tendsto (1 - g) at_top (𝓝 1),
  { rw ← sub_zero (1 : ℝ),
    exact tendsto_const_nhds.sub hg },
  have : (λ (x : ℝ), (1 - g) x * (f / (1 - g)) x) =ᶠ[at_top] f,
  { have : {(0 : ℝ)}ᶜ ∈ 𝓝 (1 : ℝ) := compl_singleton_mem_nhds zero_ne_one.symm,
    have : ∀ᶠ (x : ℝ) in at_top, (1 - g) x ∈ ({(0 : ℝ)} : set ℝ)ᶜ := lim₁ this,
    apply this.mono,
    intros x hx,
    replace hx : 1 - g x ≠ 0, by simpa using hx,
    exact mul_div_cancel' _ hx  },
  simpa using (tendsto_congr' this).mp (lim₁.mul hc)
end

That's way more better than what I could come up with :), thanks!

[Patrick Massot]

Note that your second example is much easier:

lemma tendsto_aux2 {l: ℝ} {f g: ℝ → ℝ}
  (hfg: filter.tendsto (f - g) filter.at_top (nhds 0))
  (hg: filter.tendsto g filter.at_top (nhds l)):
  filter.tendsto f filter.at_top (nhds l) :=
by convert hfg.add hg ; simp

[Ryan Lahfa]

ha

[Ryan Lahfa]

My version was :')

lemma tendsto_aux2 {u: filter ℝ} {l: ℝ} {f g: ℝ → ℝ}
  (hfg: filter.tendsto (f - g) u (nhds 0))
  (hg: filter.tendsto g u (nhds l)):
  filter.tendsto f u (nhds l) :=
begin
  rw metric.tendsto_nhds at *,
  intros ε hε,
  replace hg := hg (ε/2) (by linarith [hε]),
  replace hfg := hfg (ε/2) (by linarith [hε]),
  rw filter.eventually_iff_exists_mem at *,
  rcases hg with ⟨ s₁, hs₁, hg ⟩,
  rcases hfg with ⟨ s₂, hs₂, hfg ⟩,
  let s := s₁∩s₂,
  use s,
  split,
  exact filter.inter_mem_sets hs₁ hs₂,
  intros y hy,
  replace hg := hg _ hy.1,
  replace hfg := hfg _ hy.2,
  simp only [dist_zero_right] at hfg,
  rw [dist_eq_norm] at *,
  calc ∥f y - l∥ = ∥(f y - g y) + (g y - l)∥ : by ring
  ... ≤ ∥f y - g y∥ + ∥g y - l∥ : by sorry
  ... < ε : by sorry
end

Thanks again!

[Ryan Lahfa]

Is there a name suggestion for aux1, e.g. tendsto_of_tendsto_div_sub?

[Patrick Massot]

This seems a lot too specialized to have a name.

[Patrick Massot]

I also returned to your original question:

import analysis.specific_limits

open filter
open_locale topological_space filter

axiom ryan {l: filter ℝ} {f g: ℝ → ℝ}
  (hg: tendsto g at_top (𝓝  1)) (hc: tendsto (f / g) at_top l) : tendsto f at_top l

example : false :=
begin
  set l : filter ℝ :=  𝓟 {1},
  set f := λ x : ℝ, 1+1/(1+x^2),
  set g := λ x : ℝ, 1+1/(1+x^2),
  have hc : tendsto (f/g) at_top l,
  { rw show f = g, from rfl,
    have : g/g = 1,
    { ext x,
      apply div_self,
      dsimp [g],
      have : 0 < 1 + x^2, by linarith [sq_nonneg x],
      linarith  [one_div_pos.mpr this] },
    simp [this] },
  have hg : tendsto g at_top (𝓝 1),
  { dsimp [g],
    conv { congr, congr, skip, rw ← add_zero (1 : ℝ) },
    refine tendsto_const_nhds.add _,
    simp_rw one_div,
    exact tendsto_inv_at_top_zero.comp (tendsto_const_nhds.add_at_top $ tendsto_pow_at_top one_le_two) },
  have := ryan hg hc,
  simp at this,
  cases this with x hx,
  specialize hx x le_rfl,
  linarith [sq_nonneg x]
end

[Patrick Massot]

Explicit computation of limits are really painful, I'll go back to the adic topology.