Function Asymptotes

Stream: new members

[Callum Cassidy-Nolan]

Hello, I'm wondering if anyone has tips for making statements about functions in relation to different types of asymptotes:

image.png

After some searching in mathlib I found : https://leanprover-community.github.io/mathlib_docs_demo/analysis/asymptotics/asymptotic_equivalent.html . But It's not talking about what I'm looking for.

I think I know how to do horizontal asymptotes (just use a limit as x tends to +- infinity), but I'm not really sure how to deal with the vertical ones. If someone could give a MWE that displays a statement about each of the types of asymptotes (like the ones I've included in the image) I would be very grateful!

[Jireh Loreaux]

Here are examples of each

import topology.instances.real

open filter
open_locale topological_space

-- limit as x → 0⁺ of x⁻¹ is ∞
example : tendsto (λ x : ℝ, x⁻¹) (𝓝[>] 0) at_top := sorry

-- limit as x → 0⁻ of x⁻¹ is -∞
example : tendsto (λ x : ℝ, x⁻¹) (𝓝[<] 0) at_bot := sorry

-- limit as x → ∞ of x⁻¹ is 0
example : tendsto (λ x : ℝ, x⁻¹) at_top (𝓝 0) := sorry

-- limit as x → -∞ of x⁻¹ is 0
example : tendsto (λ x : ℝ, x⁻¹) at_bot (𝓝 0) := sorry

[Notification Bot]

Patrick Massot has marked this topic as unresolved.

[Patrick Massot]

Your definition is not general enough, your asymptote has to go through the origin with your definition.

[Patrick Massot]

So it does not cover the picture you posted.

[Eric Wieser]

I'm struggling to see how that is the case. Are you misreading a x as a * x @Patrick Massot, or am I missing something important?

[Patrick Massot]

Oh yes, I was

[Patrick Massot]

Sorry about that

[Patrick Massot]

My brain simply saw |f x - a x| where I expected |f x - a x - b|

[Patrick Massot]

without noticing the absence of computer's multiplication