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

Closed

vasnesterov wants to merge 52 commits intomasterfrom

vasnesterov/tendsto_tactic

Collaborator

vasnesterov commented Oct 31, 2024 •

edited by github-actions bot

Loading

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

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) and powers with constant real exponent.

example :
  let f := fun (x : ℝ) ↦ (4 * x)/(3 + 2 * x);
  Tendsto f atTop (nhds 2) := by
  simp only
  compute_asymptotics
  
example :
  let f := fun (x : ℝ) ↦ x^(1/2 : ℝ) / (x^(1/3 : ℝ) + x^(-1/3 : ℝ) + 18);
  Tendsto f atTop atTop := by
  simp only
  compute_asymptotics

It also supports non-numerical constants:

example (a : ℝ) (h : 0 < a) :
  let f := fun (x : ℝ) ↦ a * x;
  Tendsto f atTop atTop := by
  simp only
  compute_asymptotics
  
example :
  let f := fun (x : ℝ) ↦ Real.pi * x;
  Tendsto f atTop atTop := by
  simp only
  have : 0 < Real.pi := Real.pi_pos
  compute_asymptotics

(for more examples see compute_asymptotics.lean in tests)

Isn't it undecidable?

In general, finding the limit of a given function is undecidable problem, due to undecidability of the problem of comparing real numbers. So far I use linarith tactic for this under the hood. When it's unable to prove neither of x < y, y < x, x = y, the tactic fails.

TODO

Prove the goals of the form f =o[l] g and similarly for other O-notations.
Add sin, cos, exp, and log support.

References

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

depends on: [Merged by Bors] - feat(Analysis): radius of convergence for FormalMultilinearSeries.compContinuousLinearMap #26255
depends on: feat(Analysis/Analytic): HasFPowerSeriesOnBall.compContinuousLinearMap #23790
depends on: [Merged by Bors] - feat(Analysis/Analytic): HasFPowerSeriesOnBall.comp_sub variations #23748
depends on: feat(Analysis/Calculus): Taylor series converges to function on whole ball #23749
depends on: feat(Analysis): radius of convergence for binomial series #22538
depends on: feat(Analysis): binomial series convergence #23831
depends on: [Merged by Bors] - refactor(Data/Seq): reorganize Seq.lean #20071
depends on: [Merged by Bors] - feat(Data/Seq): update and set operations for Seq #26120
depends on: feat(Data/Seq): coinductive predicates for sequences #20241

vasnesterov added 29 commits

August 4, 2024 13:22


          after trimming

2ea7916


          make trimming computable

85ee2dd


          add MS.mul

e9f2e80


          some point

5a6a044


          Merge branch 'master' into vasnesterov/tendsto_tactic

f5bf812


          before changing wellOrdered

9c63ed3


          prove mul_isApproximation

d49f9f5


          prove inv'_isApproximation

6b16a72


          prove merge

c28ac4b


          prove mul_assoc'

e9c64e0


          prove apply_cons

a3f4e21


          prove merge_mul_comm_right

3379b2b


          before CoLits -> Seq

c966ca3


          CoList -> Seq

80fb696

fix

fb31e91


          add MS operations

283527e


          upper camel case

dd2a70e


          swap coind arguments

1129aac


          remove simp [leadingExp]

c1fc4c3


          replace -> apply at

0c4223a


          squeeze use

dd5f2b1


          use majorated API

69b7c5f


          minor


          make Seq.recOn cases_eliminator

379bab6


          rename

ef09d1e


          pass linters

69dd0e5


          translate

b9cd075


          unused variable

af4731f


          headers

2e6dbdc

vasnesterov added the WIP label


          partial trimming

d518bbf

github-actions bot reviewed

View reviewed changes

github-actions bot left a comment

Remaining comments which cannot be posted as a review comment to avoid GitHub Rate Limit

lint-style (comment with "bot fix style" to have the bot commit all style suggestions)

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2264 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2276 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2284 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2307 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2528 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2546 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2549 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2555 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2558 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2650 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2681 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2684 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2690 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

Line 2693 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Powser.lean

Line 130 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Powser.lean

Line 240 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Powser.lean

Line 258 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Powser.lean

Line 266 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Powser.lean

Line 302 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Powser.lean

Line 387 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Powser.lean

Line 523 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Operations/Powser.lean

Line 570 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/SeqLemmas.lean

Line 171 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/SeqLemmas.lean

Line 185 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/SeqLemmas.lean

Line 447 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/SeqLemmas.lean

Line 500 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/SeqLemmas.lean

Line 527 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/SeqLemmas.lean

Line 554 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/SeqLemmas.lean

Line 577 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Term.lean

Line 208 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Term.lean

Line 235 in d518bbf

simp

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Tactic/Tendsto/Multiseries/Term.lean

Line 504 in d518bbf

simp

Mathlib/Tactic/Tendsto/Meta/Trimming.lean

+                apply Approximates_sub_zero h_tl
+                rw [eventuallyEq_iff_sub]
+                eta_expand
+                simp

github-actions bot Nov 20, 2024

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

Mathlib/Tactic/Tendsto/Meta/Trimming.lean

+                apply Approximates_sub_zero h_tl
+                rw [eventuallyEq_iff_sub]
+                eta_expand
+                simp

github-actions bot Nov 20, 2024

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

Mathlib/Tactic/Tendsto/Multiseries/Operations/Add.lean

+                  have h_XY : HAdd.hAdd (α := PreMS (basis_hd :: basis_tl)) (Seq.cons (X_exp, X_coef) X_tl)
+                      (Seq.cons (Y_exp, Y_coef) Y_tl) = ?_ := by
+                    rw [add_unfold, add']
+                    simp

github-actions bot Nov 20, 2024

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

Mathlib/Tactic/Tendsto/Multiseries/Operations/Add.lean

+                  have h_YZ : HAdd.hAdd (α := PreMS (basis_hd :: basis_tl)) (Seq.cons (Y_exp, Y_coef) Y_tl)
+                      (Seq.cons (Z_exp, Z_coef) Z_tl) = ?_ := by
+                    rw [add_unfold, add']
+                    simp

github-actions bot Nov 20, 2024

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

Mathlib/Tactic/Tendsto/Multiseries/Operations/Add.lean

+                        · exact hY_comp
+                        simp only [motive]
+                        use .nil, Y_tl
+                        simp

github-actions bot Nov 20, 2024

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

    
                                    simp

                                    exact ⟨hY_tl_wo, hX_coef_wo⟩

                                  | cast j =>

                                    simp

github-actions bot Nov 20, 2024

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

    
                                  constructor

                                  · exact h_left_comp

                                  · rw [← h_right_eq.2, ← h_right_eq.1.1] -- copypaste

                                    simp

github-actions bot Nov 20, 2024

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

    
                                · intro j

                                  cases j using Fin.lastCases with

                                  | last =>

                                    simp

github-actions bot Nov 20, 2024

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

    
                                    simp

                                    exact ⟨hY_tl_wo, hX_coef_wo⟩

                                  | cast j =>

                                    simp

github-actions bot Nov 20, 2024

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

Mathlib/Tactic/Tendsto/Multiseries/Operations/Mul.lean

    
                    cases' b with b_exp b_coef b_tl

                    · apply Approximates_nil at hb_approx

                      left

                      simp

github-actions bot Nov 20, 2024

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

vasnesterov added 2 commits

November 21, 2024 16:10


          different filters

dc80c17


          before merge

e79c1a1

vasnesterov mentioned this pull request

[Merged by Bors] - refactor(Data/Seq): mark Seq.recOn with cases_eliminator #19829

Closed

wip

5cef1e9

leanprover-community-bot-assistant added the merge-conflict label

vasnesterov mentioned this pull request

[Merged by Bors] - feat(Data/Seq): structural lemmas #19859

Closed

1 task

vasnesterov added 7 commits

December 15, 2024 00:42


          zpow

cda1ea9


          naming

fa290d1


          remove FlatZero

d3c8d5b


          use ofScalars in Powser

3fc0c5e


          use Ring.choose in Pow

302d1d8


          generalize binomial series

84eb083


          update Mathlib Tactic

42b3ada

vasnesterov mentioned this pull request

feat(Analysis): binomial series convergence #20011

Closed

2 tasks

vasnesterov mentioned this pull request

feat(Data/Seq): coinductive predicates for sequences #20241

Closed

1 task

vasnesterov added 4 commits

March 1, 2025 03:00


          remove wrong comment


          bump Seq.lean

2690c4a


          mk_all

482924a


          linters

e738059

vasnesterov changed the title ~~feat(Tactic): Tactic for computing asymptotics of real functions~~ feat(Tactic): tactic for computing asymptotics of real functions

mathlib4-dependent-issues-bot added the blocked-by-other-PR label

Collaborator

mathlib4-dependent-issues-bot commented May 8, 2025 •

edited

Loading

This PR/issue depends on:

vasnesterov mentioned this pull request

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

Open

7 tasks

Collaborator Author

vasnesterov commented Aug 12, 2025

This PR has been migrated to a fork-based workflow: #28291

vasnesterov added the migrated-to-fork label

vasnesterov closed this

YaelDillies deleted the vasnesterov/tendsto_tactic branch

August 17, 2025 11:42

vasnesterov mentioned this pull request

[Merged by Bors] - feat(Data/Seq): coinductive predicates for sequences #28874

Closed

1 task

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

blocked-by-other-PR merge-conflict migrated-to-fork t-meta WIP