Proving that function of reciprocals have vertical asymptote

Stream: new members

[Brando Miranda]

I want to prove in Lean4 the following theorem as a basic sanity check (not trying to generalize it yet, just as is):

thm: Show that f(x) = 2 / (x^2 + x - 6) has 2 vertical asymptotes at x=-3, x=2.

This is my current attempt

/-
Strategy

define: f

lemma: (x^2 + x - 6) = (x + 3)(x - 2)

define: vertical asymptote, as lim_{x->val} f(x) = infity
(on either side i.e. vertical asymptote if goes to infinity if it does from left or right)

Theorem1: Show that f(x) = 2 / (x^2 + x - 6) has 2 vertical asymptotes at x=-3, x=2.
proof:
rewrite f -> 2 / (x + 3)(x - 2)
cases:
1. show lim_{x -> -3} f(x) = infinity
2. show lim_{x -> 2} f(x) = infinity
end
-/

import Mathlib.Tactic.Linarith
-- import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Data.Real.Basic
-- import Mathlib.Analysis.Calculus.Tendsto

noncomputable def f (x : ℝ) : ℝ := 2 / (x^2 + x - 6)

-- Preliminary lemma that might be used to simplify expressions or directly in proof
lemma denom_factorization (x : ℝ) : x^2 + x - 6 = (x - 2) * (x + 3) :=
by ring

-- thm: Show that f(x) = 2 / (x^2 + x - 6) has 2 vertical asymptotes at x=-3, x=2.
-- thm: Show that lim_{x -> -3} f(x) = infinity /\ lim_{x -> 2} f(x) = infinity
theorem vertical_asymptotes_thm1 :

how does one do this?

What I am stuck in is that there seems to be multiple limit/tendsto functions and I am worried about type coercion (and my general lack of experience in Lean makes it hard for me to try things).

e.g.,

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/Order/LeftRightLim.html#Function.leftLim

and

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecificLimits/Basic.html

but I'm really only interested in the real numbers version of this theorem.

[Kevin Buzzard]

Can you offer a rigorous definition of vertical asymptote? Your claim lim_{x -> -3} f(x) = infinity will not be true for your function, because as x tends to -3 from above the limit will be -infinity. Does -1/x^2 have a vertical asymptote at x=0?

[Kevin Buzzard]

Does 1/(x sin(1/x)) have a vertical asymptote at x=0?

[Brando Miranda]

Kevin Buzzard said:

Can you offer a rigorous definition of vertical asymptote? Your claim lim_{x -> -3} f(x) = infinity will not be true for your function, because as x tends to -3 from above the limit will be -infinity. Does -1/x^2 have a vertical asymptote at x=0?

You are correct. My theorem is wrong (doesn't match what I drew on paper). My apologies. As you correctly identified, I am trying to find the correct Mathlib definitions (with the right types) to define vertical asymptote. The definition of vertical asymptote I had in mind was:

A vertical asymptote of a graph is := "a vertical line x = a where the graph tends toward positive or negative infinity as the inputs approach a".

Therefore the theorem I wanted to write (informally) is (with my specific f):

-- definition f: f(x) = 2 / (x^2 + x - 6)
-- lemma denom_factorization (x : ℝ) : x^2 + x - 6 = (x - 2) * (x + 3) := by ring
-- definition Func_has_Vertical_Asymptote: (f: Real -> Real) (a : Real) : lim_{x -> a} = +- infinity
-- theorem Has_two_vertical_asymptotes:  Func_has_Vertical_Asymptote f 2 /\ Func_has_Vertical_Asymptote f -3 := by sorry

but I'm struggling to understand how or which limit function to use. Given there are so mean that seem correct, filters, metric spaces, reals, etc. What I'd personally do is use Reals given, the type of my function f.

[Kevin Buzzard]

I am still not happy with the definition (in the sense that I don't know what "tending towards x or y as the inputs approach z" even means). Does 1/x(sin(1/x)) have a vertical asymptote at x=0? Can you write an epsilon-delta-like definition of what you mean by "tending to x or y"?

[Kevin Buzzard]

Once we have a rigorous mathematical definition it will be fine translating it into Lean, but right now I don't feel like I have a rigorous definition of this concept.

[Brando Miranda]

Kevin Buzzard said:

I am still not happy with the definition (in the sense that I don't know what "tending towards x or y as the inputs approach z" even means). Does 1/x(sin(1/x)) have a vertical asymptote at x=0? Can you write an epsilon-delta-like definition of what you mean by "tending to x or y"?

I will assume you meant g(x) = 1/(x sin(1/x)) (and not 1/x sin(1/x)). I appreciate the issue i.e. as x -> 0 then 1/x->+-infinity but sin(1/x) oscillates very rapidly between +-1 (rapidly meaning sin'(x) = -cos(1/x)x^-2 compared to x' = 1). What I would have personally done is allow g(x) to have a vertical asymptote since the other term is always bounded, even if it oscillates. But that messes the traditional definition of limit, which usually goes to a specific concrete value L i.e. lim_{x->a} f(x) = L. Therefore, we should stick to the standard epsilon-delta definition of limits and not allow 1/(x sin(1/x))to have a vertical asymptote. It doesn't seem standard to change the traditional definition of limit and my goal is use Mathlib as much as possible.

[Kevin Buzzard]

So what is your definition? Because if a sequence x_,n is tending to zero by jumping between positive and negative reals (which is a perfectly allowable way to tend to zero) then 1/x_n will also be jumping around between large positive and large negative numbers which you've just disallowed. Does the function f(x) = 1/x if x is rational and -1/x if x is irrational have a vertical asymptote?

Let me try and clarify. I do not actually want you to answer that question. Your personal opinion on whether that function has a vertical asymptote will get us nowhere. I want you to give me a formal mathematical definition of "has a vertical asymptote" which does not contain the word "limit" but which instead begins something like "for all epsilon > 0...". Something that lean can actually work with. Just to be clear -- have you seen the formal mathematical definition of a limit or a derivative? The point I'm trying to make with the pathological examples of functions I'm throwing out is that you can't just say "look at the picture" because a general function is totally wild and doesn't look like the pictures of functions with asymptotes which you see in the high school textbooks. Lean can't work with pictures or ideas or vague concepts like "tends to +infinity or -infinity", it can't work with "Kevin suggests a function and Brando comes up with their own opinion about whether it has an asymptote and then it's Kevin's move again" -- we need to see a definition with absolutely no hand-waving and no vague usage of the word "limit" (eg no meaningless phrase "limit is this or that") before we can even state the theorem. We need epsilons and deltas, not Isaac Newton mathematics. This is not physics.

[Brando Miranda]

Hi Kevin (apologies for delay, wasn't around for a bit but I'm back).

The definition of limit I was expecting is the standard one for real numbers \forall \eps >0, \exists delta >0 s.t. if 0 < |x - c| < delta ==> 0 < | f(x) - L | < eps meaning lim_{x->c} f(x) = L where L is a constant real. I expected such a definition to exist in lean that was compatible with the definition of extended reals (using +- infinity, I was thinking of the formal definition Walter Rudin had in his textbook). So that I could prove my function had to limits that go to plus or minus infinity at the corresponding two points -3 and 2. So I am defining formally Vertical Asymptote as def VA (f : R -> R) := lim f = +- infinity. If that is wrong I'm happy to correct it.

I am happy (especially as I am learning lean) to define limits from scratch. I currently working on it right now and happy to share my attempt in a bit.

[Jireh Loreaux]

Note: your epsilon definition doesn't work to define lim f = +infinity because you can't choose L = +infinity. So here, if you want Kevin to be able to answer you, you'll need to provide "the formal definition Walter Rudin had in his textbook", or at least specify exactly which of Rudin's textbooks you mean, and on what page the definition can be found (but it's better to just reproduce it here).

[Kevin Buzzard]

My main objection was not about the definition of limit, but the concept of "limit is x or y" (a phrase you used more than once). Does this mean "either limit is x or limit is y" (which I know how to translate into lean) or does it include "function is hopping between x and y and is kind of tending to both of them" (in which case we need an epsilon delta definition of what you mean).

[Kevin Buzzard]

Basically the sooner we stop writing large walls of text and you just post three lines of LaTeX actually saying rigorously what you mean by a vertical asymptote without using the phrase "limit is x or y" and ideally using epsilons and deltas, the sooner we can proceed.

[Jeremy Tan]

Kevin Buzzard said:

I am still not happy with the definition (in the sense that I don't know what "tending towards x or y as the inputs approach z" even means). Does 1/x(sin(1/x)) have a vertical asymptote at x=0? Can you write an epsilon-delta-like definition of what you mean by "tending to x or y"?

I think we can crib Wikipedia's definition: there is a vertical asymptote of f at x if Tendsto f (\MCN[>] x) atTop or the three variants replacing > with < or atTop with atBot or both

[Kevin Buzzard]

So you think the definition is "either tends to +infinity or -infinity as we tend to x from above, and also either tends to +infty or -infinity as we tend to x from below". That sounds like a reasonable definition to me.

[Richard Osborn]

See docs#Filter.tendsto_inv₀_nhdsWithin_ne_zero for a proof that $1/x$ has a vertical asymptote at $0$.

[Patrick Massot]

That is yet another interpretation of “vertical asymptote”.

[Kevin Buzzard]

Right: 1/x if x is rational and -1/x if x is irrational satisfies that bornology criterion but not Jeremy's criterion.

[Brando Miranda]

Ok I made some progress on my current proof attempt. I defined limit to infinity as unbounded limit and only considering the right limit for simplicity:

import Mathlib.Data.Real.Basic

-- define 1/x (reciprocal) for reals
noncomputable def f (x : ℝ ):  ℝ := x⁻¹
#check f

-- -- unit test that f 1 = 1, f 2 = 1/2
theorem test_f1 : f 1 = 1 := by simp[f]
theorem test_f2 : f 2 = 2⁻¹ := by simp[f]
#print test_f1
#print test_f2

-- The limit of f x as x approaches c+ from the right is +infinity i.e., limit is unbounded from the right
-- i.e., lim_{x -> c+} f(x) = +infinity
def has_unbounded_limit_right (f: ℝ -> ℝ) (c : ℝ) : Prop :=
  ∀ M : ℝ, 0 < M → ∃ δ, 0 < δ ∧ ∀ x : ℝ, 0 < x - c ∧ x - c < δ → M < f x

theorem reciprocal_has_unbounded_limit_right : has_unbounded_limit_right f 0 := by
  intro M hM
  use M⁻¹
  -- split (what did scott want with this, read)
  constructor
  . rwa [inv_pos]
  . rintro x ⟨h_x_pos, h_x_lt_δ⟩
  -- rewrite both hypothesis using substraction zero
    rw [sub_zero] at h_x_pos h_x_lt_δ
    unfold f
    -- multiply both sides of h_x_lt_δ by x⁻¹ on the left using mul_lt_mul_right
    #check mul_lt_mul_right

I've tried a bunch of things after -- multiply both sides of h_x_lt_δ by x⁻¹ on the left using mul_lt_mul_right with apply?, exact?, rw?, more + copilot, GPT4, Moogle, mathlib docs etc. I just can't seem to find the right tactic to do what I want to do. Does someone know how to get Lean to do multiply both sides of h_x_lt_δ by x⁻¹ on the left using mul_lt_mul_right?

(todo: running out of time this morning but I can paste my pen and pencil proof in a bit)

[Richard Osborn]

exact? was able to find exact (lt_inv hM h_x_pos).mpr h_x_lt_δ which closes the proof.

[Richard Osborn]

Sorry, were you asking specifically for this?
rw [← mul_lt_mul_left (inv_pos.mpr h_x_pos)] at h_x_lt_δ

[Brando Miranda]

I found a couple of proofs I'm happy with. Thanks y'all!

-- import real numbers form mathlib
import Mathlib.Data.Real.Basic

noncomputable def f (x : ℝ) : ℝ := x⁻¹
#print f
#check f
#check f 1
-- #eval f 1
-- theorem any_R : ℝ -> R := λ x : ℝ, x -- TODO
theorem unit_test_f_1 : f 1 = 1 := by simp [f]
theorem unit_test_f_2 : f 2 = 1/2 := by simp [f]
noncomputable def f' (x : ℝ) : ℝ := 1/x
theorem units_f_eq_f' : ∀ x : ℝ , f x = f' x := by simp [f, f']
#print units_f_eq_f'

-- lim_{x -> c+} f(x) = +infinity := ∀ M > 0, ∃ δ > 0, ∀ x : ℝ, 0 < x - c < δ → f(x) > M
def unbounded_limit (f : ℝ -> ℝ) (c : ℝ) : Prop :=
  ∀ M : ℝ, 0 < M → ∃ δ : ℝ, 0 < δ ∧ ∀ x : ℝ, 0 < x - c ∧ x - c < δ → M < f x

-- show 1/x is unbounded as x -> 0 (or 1/x has a veritcal asymptote at x = 0)
theorem limit_of_reciprocal_of_x_is_unbounded: unbounded_limit f 0 := by
  unfold unbounded_limit f
  -- choose M : ℝ and is M > 0
  intro M h_M_pos
  -- choose delta = M⁻¹ by a tactic
  use M⁻¹
  -- deconstruct the constructor Left ∧ Right = And(Left, Right) to Left, Right using a tactic
  apply And.intro
  . exact (by simp [h_M_pos]) -- TODO try to find the lemma in mathlib to prove this
  . intro x ⟨h_x_pos, h_x_lt_M⟩
    -- rewrite x - 0 to x using a tactic for sub
    rw [sub_zero] at h_x_pos h_x_lt_M
    -- using rewrite do M < x⁻¹ → M * x < x⁻¹ * x by mulitpling both sides by x on the right
    -- #print mul_lt_mul_right -- (a0 : 0 < a) : b * a < c * a ↔ b < c
    rw [←mul_lt_mul_right h_M_pos] at h_x_lt_M
    -- #print mul_inv_cancel
    -- mul_inv_cancel: a ≠ 0 → a * a⁻¹ = 1
    nth_rewrite 2 [mul_comm] at h_x_lt_M
    have h_M_neq_zero : M ≠ 0 := ne_of_gt h_M_pos
    rw [mul_inv_cancel h_M_neq_zero] at h_x_lt_M
    -- multiply both sides by x⁻¹ on the left
    have h_x_inv_pos : 0 < x⁻¹ := inv_pos.mpr h_x_pos
    rw [← mul_lt_mul_left h_x_inv_pos] at h_x_lt_M
    -- apply associativity of mul
    rw [← mul_assoc] at h_x_lt_M
    -- mul_inv_cancel: a ≠ 0 → a * a⁻¹ = 1
    nth_rewrite 2 [mul_comm] at h_x_lt_M
    -- cancel the x * x⁻¹ to 1
    have h_x_neq_zero : x ≠ 0 := ne_of_gt h_x_pos
    rw [mul_inv_cancel h_x_neq_zero] at h_x_lt_M
    -- apply 1 * M = M
    rw [one_mul] at h_x_lt_M
    rw [mul_comm] at h_x_lt_M
    rw [one_mul] at h_x_lt_M
    assumption

[Brando Miranda]

I want to do two things however:

1. I want to change the statement to say that 1/x has a single asymptote from the right (as I formally defined). How do I change the theorem (or extend it) and state I want prove there is a single right asymptote for some x value?
2. I would like to change the theorem to work the unbounded limit definition in mathlib. This is the new skill I want to obtain, using matlib as much as possible. I feel my definition although fine probably already exists in mathlib. How do I do this? Or what is a starter/general tips so I can give it a shot on my current proof.

Thanks!

Side: note, is there a good lean hammer or one to be released? like the one in Isabelle that is amazing?

[Jireh Loreaux]

regarding (2), you're unbounded_limit f c would be written Tendsto f (𝓝[>] c) atTop with open Filter Topology.

[Jireh Loreaux]

Regarding (1), it's not clear to me what you mean. Do you mean that there exists a unique c such that unbounded_limit (fun x ↦ 1/x) c?

[Jireh Loreaux]

@Brando Miranda Here's a proof for (2) that the version I gave is equivalent to yours:

import Mathlib

-- lim_{x -> c+} f(x) = +infinity := ∀ M > 0, ∃ δ > 0, ∀ x : ℝ, 0 < x - c < δ → f(x) > M
def unbounded_limit (f : ℝ -> ℝ) (c : ℝ) : Prop :=
  ∀ M : ℝ, 0 < M → ∃ δ : ℝ, 0 < δ ∧ ∀ x : ℝ, 0 < x - c ∧ x - c < δ → M < f x

-- is Mathlib really missing this?
lemma Set.Ioo_inter_Ioi_of_le {α : Type*} [Preorder α] {a b c : α} (h : a ≤ c) :
    Set.Ioo a b ∩ Set.Ioi c = Set.Ioo c b := by
  ext x
  simp only [mem_inter_iff, mem_Ioo, mem_Ioi, and_comm (a := c < x), and_congr_left_iff,
    and_iff_right_iff_imp]
  exact fun hc _ ↦ h.trans_lt hc

open Filter Topology
example (f : ℝ → ℝ) (c : ℝ) : unbounded_limit f c ↔ Tendsto f (𝓝[>] c) atTop := by
  rw [Metric.nhdsWithin_basis_ball.tendsto_iff (atTop_basis_Ioi' 0), unbounded_limit]
  simp only [Real.ball_eq_Ioo, and_imp]
  peel with ε _hε δ hδ x
  rw [Set.Ioo_inter_Ioi_of_le (by linarith [hδ.le])]
  simp [sub_lt_iff_lt_add']

[Jireh Loreaux]

All the real mathematics happens with the single rewrite rw [Metric.nhdsWithin_basis_ball.tendsto_iff (atTop_basis_Ioi' 0)]. This declaration, namely docs#Filter.HasBasis.tendsto_iff is the way to convert between ε-δ-style limits and docs#Filter.Tendsto statements. For this, you need a basis for the corresponding filter.

[Jireh Loreaux]

Some common bases include:

• docs#Metric.nhds_basis_ball, which is the usual basis for the filter 𝓝 a (this is docs#nhds)
• docs#Metric.nhdsWithin_basis_ball, this is the usual basis for the filter for 𝓝 a but restricted to a set s, so in particular this works for 𝓝[>] a (where s := Set.Ioi a), or 𝓝[≠] a(where s := {a}ᶜ), and this allows you to take one-sided limits, or limits at point (but excluding the limiting value).
• docs#Filter.atTop_basis, the usual basis for the filter at infinity (use atBot for negative infinity). But there are several variants, docs#Filter.atTop_basis', docs#Filter.atTop_basis_Ioi and docs#Filter.atTop_basis_Ioi', and you'll note that I used the last one above because in your definition of unbounded_limit you required M > 0.

[Jireh Loreaux]

There are plenty more filter bases, but these are the only you need to talk about the various kinds of limits one encounters in an introductory real analysis class.