feat(Tactic): tactic for computing asymptotics of real functions

[vasnesterov]

It's an auxiliary PR which implements the entire compute_asymptotics tactic. I am spliting it into multiple small PRs.

---

Tactic description: https://vasnesterov.github.io/compute_asymptotics

Zulip announcement: #announce > New tactic: `compute_asymptotics`

In this PR I implement the compute_asymptotics tactic. Its purpose is to compute asymptotics of functions from ℝ to ℝ. So far it is able to compute the limit of any function constructed using arithmetic operations (+, -, *, /, inversion), powers, logarithms, and exponents.

import Mathlib.Tactic.ComputeAsymptotics

open Real Filter Topology Asymptotics

example : Tendsto (fun (x : ℝ) ↦ (1 + 6 * x⁻¹) ^ (7 * x)) atTop (𝓝 (exp 42)) := by
  compute_asymptotics

example : (fun x ↦ x - 1 - log x) ~[𝓝[≠] 1] (fun x ↦ (x - 1) ^ 2 / 2) := by
  compute_asymptotics

example (a b : ℝ) (h : a < b) :
    (fun x ↦ (x + x * log x) ^ a) =O[atTop] (fun x ↦ (x / log x) ^ b) := by
  compute_asymptotics

example :
    (fun x ↦ log x) =o[𝓝[>] 0] (fun x ↦ Real.pi / (exp (Real.log 2 * x) - 1)) := by
  compute_asymptotics

For more examples see compute_asymptotics.lean in tests.

TODO

• Different domains in compute_limit as well.
• Trigonometric functions and Gamma-function.

References

I am basically implementing this article about computing asymptotics in Isabelle by Manuel Eberl.

Small PRs

Here's a few smaller PRs coming from this one, ordered by importance:

• depends on: feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq: FriendlyOperation API #35072
• depends on: feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq: FriendlyOperation API #37342
• depends on: [Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): Multiseries definition and structural lemmas #34922
• depends on: [Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): Majorized predicate #34356
• depends on: [Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): WellFormedBasis lemmas #34422
• depends on: [Merged by Bors] - feat(Tactic/ComputeAsymptotics): lemmas for converting different goals to Tendsto f atTop l #34403
• depends on: [Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq #34311

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq: FriendlyOperation API #35072
• feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq: FriendlyOperation API #37342
• [Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): Multiseries definition and structural lemmas #34922
• [Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): Majorized predicate #34356
• [Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): WellFormedBasis lemmas #34422
• [Merged by Bors] - feat(Tactic/ComputeAsymptotics): lemmas for converting different goals to Tendsto f atTop l #34403
• [Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq #34311
  By Dependent Issues (🤖). Happy coding!

[grunweg]

Hi! I'm still excited about your PR and this tactic. If/when you split out further pieces into reviewable PRs, I can try to find a reviewer for them.

[grunweg]

Hi! I'm still excited about your PR and this tactic. If/when you split out further pieces into reviewable PRs, I can try to find a reviewer for them.

By the way, this offer still stands, whenever you find time for this. (There's no rush on my side - but I'm happy to help.)

[vasnesterov]

@grunweg Thanks for the support! I'm planning to do a major refactoring that will improve the tactic on functions with complex cancellations. For example, my tactic can’t yet prove this limit:

example :
    let f := fun x ↦ exp x * ((x + 1)⁻¹ - (x + 1)⁻¹)
    Tendsto f atTop (𝓝 0) := by
  compute_asymptotics

I don’t think such functions are very important in practice, but it still feels wrong that my tactic can’t handle most of the limits in Section 8 of Gruntz’s thesis. After that I'll start splitting this into smaller pieces and PRing them

[ocfnash]

@vasnesterov I've just had a quick look over this PR and I have a few remarks and questions as follows:

1. Thank you for writing this. We would absolutely love to have a tactic with these abilities in Mathlib.
2. IMHO it is more important for this to be maintainable and in master than maximally featured.
3. It looks like most of the maintenance burden would stem from the contents of the Multiseries folder. Can you very briefly summarise what this is and why it is necessary and what design choices you see?
4. Could you merge master to make it a bit easier to see the changes?
5. Could you split out some small PRs with the library code (i.e., outside of the Tactic folder)?
6. Could you open a small PR with the factorial extension to norm_num?

[vasnesterov]

@ocfnash

1. Thanks!
2. I completely agree. But I was going to add the feature I mentioned above anyway, and I don't want to double the reviewers' workload.
3. Multiseries is a key object used by the tactic. It's a generalization of asymptotic series. See this paper for details.
4. Currently working on it!
5. I've already done that. The only (almost) code not yet in master is the tactic itself. The diff displayed here is quite outdated.
6. That's also already in master.

[ocfnash]

@vasnesterov Thanks, this all sounds marvelous. I can't yet tell what will be the outcome yet but I can say several of us our very excited about a tactic like this and that I look forward to having a clearer diff.

Thanks so much!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.