Zulip Chat Archive

Stream: mathlib4

Topic: f = o(g) -> f > g only on bounded set

Jeremy Tan (Feb 05 2026 at 01:28):

@Kevin Buzzard said in #general > sloplib @ πŸ’¬ that I should prove #34845 through this lemma. But this lemma does not seem to be in mathlib

I think that finite_abs_eval_lt_of_degree_lt should be deduced from the claim that if one function is little-o of another one then the smaller one only beats the bigger one on a bounded set rather than grinding it out in the specific case of polynomials as Aristotle has seemed to have done

Jeremy Tan (Feb 05 2026 at 01:42):

In particular you also need to prove the behaviour atBot; mathlib currently only has atTop lemmas

Bolton Bailey (Feb 05 2026 at 02:24):

You may already be working on this, but I asked Claude to refactor out some of the haves and do a generalization along these lines, and I got this output, perhaps it's useful to you.

open Filter Topology in
/-- If `deg P < deg Q`, then `P(x) / Q(x) β†’ 0` as `x β†’ ±∞`. -/
lemma div_tendsto_zero_of_degree_lt_atTopBot (P Q : β„š[X]) (h : P.degree < Q.degree) :
    Tendsto (fun x ↦ P.eval x / Q.eval x) (atTop βŠ” atBot) (𝓝 0) := by
  have l₁ : ((P.comp (-X)).degree < (Q.comp (-X)).degree) := by simp [h]
  apply Tendsto.sup
  Β· exact div_tendsto_zero_of_degree_lt _ _ h
  Β· convert (div_tendsto_zero_of_degree_lt _ _ l₁).comp tendsto_neg_atBot_atTop using 2
    simp

open Filter Topology in
/-- If `f` tends to `0` as `x β†’ ±∞`, then `|f x| < 1` outside a bounded interval. -/
lemma exists_bounds_abs_lt_one_of_tendsto_zero {f : β„š β†’ β„š}
    (hf : Tendsto f (atTop βŠ” atBot) (𝓝 0)) :
    βˆƒ M₁ Mβ‚‚, βˆ€ x, x ≀ M₁ ∨ Mβ‚‚ ≀ x β†’ |f x| < 1 := by
  have hf' := hf.abs
  simp only [abs_zero] at hf'
  replace hf' := hf'.eventually (gt_mem_nhds zero_lt_one)
  rw [eventually_sup, eventually_atTop, eventually_atBot] at hf'
  obtain ⟨⟨Mβ‚‚, hMβ‚‚βŸ©, ⟨M₁, hMβ‚βŸ©βŸ© := hf'
  exact ⟨M₁, Mβ‚‚, fun x hx ↦ hx.elim (hM₁ _) (hMβ‚‚ _)⟩

open Filter Topology in
/-- For integers outside a finite interval, if `P(x) β‰  0` and the ratio `|Q(x)/P(x)| < 1` for
rationals outside that interval, then `|Q(x)| < |P(x)|`. -/
lemma abs_eval_lt_of_not_mem_Ioo {P Q : β„€[X]}
    {M₁ Mβ‚‚ : β„€} (hM : βˆ€ (x : β„š), x ≀ M₁ ∨ Mβ‚‚ ≀ x β†’
      |(Q.map (Int.castRingHom β„š)).eval x| / |(P.map (Int.castRingHom β„š)).eval x| < 1)
    {x : β„€} (hx : x βˆ‰ Finset.Ioo M₁ Mβ‚‚) (hPx : P.eval x β‰  0) :
    |Q.eval x| < |P.eval x| := by
  have hx' : (x : β„š) ≀ M₁ ∨ (Mβ‚‚ : β„š) ≀ x := by
    simp only [Finset.mem_Ioo, not_and_or, not_lt, Int.cast_le] at hx ⊒
    exact hx
  specialize hM _ hx'
  simp only [eval_intCast_map, Int.cast_eq, eq_intCast] at hM
  rw [div_lt_oneβ‚€ (by positivity)] at hM
  exact_mod_cast hM

open Filter Topology in
/-- If `deg Q < deg P`, there are only finitely many integers `x` where `|P(x)| ≀ |Q(x)|`. -/
lemma finite_abs_eval_lt_of_degree_lt {P Q : β„€[X]} (h : Q.degree < P.degree) :
    {x | |P.eval x| ≀ |Q.eval x|}.Finite := by
  let c := Int.castRingHom β„š
  have hdeg : (Q.map c).degree < (P.map c).degree := by
    simpa [degree_map_eq_of_injective c.injective_int]
  obtain ⟨M₁, Mβ‚‚, hM⟩ := exists_bounds_abs_lt_one_of_tendsto_zero
    ((div_tendsto_zero_of_degree_lt_atTopBot _ _ hdeg).abs.congr fun _ ↦ abs_div _ _)
  simp only [abs_div, abs_abs] at hM
  have hM' : βˆ€ (x : β„š), x ≀ ⌊Mβ‚βŒ‹ ∨ ⌈Mβ‚‚βŒ‰ ≀ x β†’
      |(Q.map c).eval x| / |(P.map c).eval x| < 1 := fun x hx' ↦
    hM x (hx'.elim (fun l ↦ .inl (l.trans (Int.floor_le M₁)))
      fun l ↦ .inr ((Int.le_ceil Mβ‚‚).trans l))
  refine (Finset.Ioo ⌊Mβ‚βŒ‹ ⌈Mβ‚‚βŒ‰ βˆͺ P.roots.toFinset).finite_toSet.subset fun x hx ↦ ?_
  contrapose! hx
  rw [Set.mem_setOf_eq, not_le]
  rw [SetLike.mem_coe, Finset.mem_union, not_or, Multiset.mem_toFinset, mem_roots', not_and] at hx
  exact abs_eval_lt_of_not_mem_Ioo hM' hx.1 (hx.2 (ne_zero_of_degree_gt h))

Bolton Bailey (Feb 05 2026 at 02:25):

I think it meets the general description of "deduced from the claim that if one function is little-o of another one then the smaller one only beats the bigger one on a bounded set", but perhaps there are other "slop" things that someone else would find :shrug:

Jeremy Tan (Feb 05 2026 at 02:26):

Come to think of it, the more general claim is only guaranteed to be true along the filter used in the little-o. Think Airy's Ai and Bi – the two functions oscillate around each other on the negative axis, but Bi dominates Ai on the positive axis

Jeremy Tan (Feb 05 2026 at 02:29):

Is Kevin asking me to ditch AI entirely for this one?

Jeremy Tan (Feb 05 2026 at 06:53):

OK, I tried a different approach. #34868 adds missing atBot and asymptotics lemmas for Analysis.Polynomial.Basic

Last updated: Feb 28 2026 at 14:05 UTC