Tendsto on divison of linear functions

Stream: Is there code for X?

[EdwardW]

Hi :)

Was trying something of the sort:

theorem linear_div_tendsto {𝕂 : Type u_1} [RCLike 𝕂] (a b c d : 𝕂) (hc : c ≠ 0) :

    Tendsto (fun (x:ℝ) ↦ ‖(a * x + b) / (c * x + d)‖) atTop (nhds ‖a/c‖) := by sorry

This can be solved by dividing through by $x$, but that requires $x \neq 0$ and is messy algebra. I couldn't find anything particularly helpful in Mathlib. Polynomial.div_tendsto_leadingCoeff_div_of_degree_eq is the closest I can find, but that required an ordered field, which is not necessary here.

Thanks!

[Kevin Buzzard]

If I were doing this from first principles on paper I'd subtract and add a/c from ax+b/cx+d to get a/c+(bc-ad)/c(cx+d) and then just prove that the latter tends to zero.

[EdwardW]

Yes exactly, I guess I'll do it the hard way, I might investigate the tendsto API as that could do with some additional infrastructure

[Bhavik Mehta]

I'd do the proof by dividing through by x, using the fact that (ax+b)/(cx+d) =ᶠ[atTop] (a+b/x)/(c+d/x), and then the denominator is eventually nonzero too. Once you state everything in terms of eventually atTop, you can filter upwards and get x != 0 as a hypothesis, then field_simp + ring should make the algebra really easy

[EdwardW]

Seems like more effort than Kevin's way, but yes that seems like the way I was going to do it originally

[Kevin Buzzard]

It looks to me like about the same amount of effort. The trick is to move away from (ax+b)/(cx+d) (which there won't be any lemmas about, I guess) to functions like b/x or constant functions, which hopefully there will be lemmas about (and then apply results about sum of limits is limit of sums etc)

[EdwardW]

For sure, saying that it would definitely be useful to have division of two polynomials, or higher degree polynomials/arbitrary polynomials become really messy

[Kevin Buzzard]

Can you formalise the statement about division of two polynomials which you think we should have?

[EdwardW]

Probably

theorem Polynomial.RCLike.div_tendsto_leadingCoeff_div_of_degree_eq {𝕜 : Type u_1} [RCLike 𝕜]
    (P Q : 𝕜[X]) (hdeg : P.degree = Q.degree) : Tendsto
    (fun x : ℕ ↦ eval ↑x P / eval ↑x Q) atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff)) := by sorry

?

Perhaps I am mistaken, but this doesn't seem trivial, in fact I was working on it just now and it seems like tendsto support for RCLike is somewhat lacking, perhaps this is because this is covered by another typeclass?

[Jireh Loreaux]

I think it's not the statement you want. There's no reason to restrict to sequences.

import Mathlib

open Bornology Filter Topology Polynomial

theorem Polynomial.tendsto_div_cobounded_of_degree_eq
    {𝕜 : Type*} [NontriviallyNormedField 𝕜] (P Q : 𝕜[X]) (hdeg : P.degree = Q.degree) :
    Tendsto (fun x : 𝕜 ↦ eval x P / eval x Q) (cobounded 𝕜) (𝓝 (P.leadingCoeff / Q.leadingCoeff)) := by
  sorry

[Jireh Loreaux]

Actually, maybe you only need NormedField because of Filter.tendsto_inv₀_cobounded

[EdwardW]

You are correct, I wasn't sure how to generalise my idea, I suppose then that mine is obtained by composition on an algebraMap. Would it be helpful if I proved this statement?

[EdwardW]

/ attempted to :face_with_peeking_eye:

[Bhavik Mehta]

I just came across docs#div_tendsto_leadingCoeff_div_of_degree_eq which looks really similar to this, although it's for x atTop rather than cobounded. Maybe it helps here, or for others coming across this thread in the future

[Anatole Dedecker]

Yes, in an ideal world everything would follow docs#Polynomial.isEquivalent_atTop_lead. I remember at the time I added this the most annoying part in using it was computing concrete things about concrete polynomials, do we have tactics to do that now?

[EdwardW]

Hmm probably not, it would be nice to be corrected. I suppose ring tactics etc would help though