[Merged by Bors] - feat(Tactic/ComputeAsymptotics): lemmas for converting different goals to `Tendsto f atTop l` by vasnesterov · Pull Request #34403 · leanprover-community/mathlib4

vasnesterov · 2026-01-25T11:23:09Z

Prove lemmas we use in compute_asymptotics to reduce various asymptotic goals to the case Tendsto f atTop l.

This is a part of the compute_asymptotics tactic (#28291).

depends on: [Merged by Bors] - chore(Analysis/Asymptotics): remove unnecessary hypothesis from isEquivalent_of_tendsto_one #34389
depends on: [Merged by Bors] - feat(Algebra/Order): multiplicative versions of lemmas on (pre)images of intervals under group operations #34561

github-actions · 2026-01-25T11:24:19Z

PR summary f7ee1844c2

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Asymptotics.Lemmas	1432	1445	+13 (+0.91%)
Mathlib.Topology.Algebra.Group.Basic	1021	1024	+3 (+0.29%)

Import changes for all files

Files	Import difference
`Mathlib.Tactic` `Mathlib.Topology.Algebra.Valued.ValuativeRel`	1
112 files `Mathlib.Algebra.Category.Ring.Topology` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.AffineTransitionLimit` `Mathlib.AlgebraicGeometry.Artinian` `Mathlib.AlgebraicGeometry.ColimitsOver` `Mathlib.AlgebraicGeometry.Cover.Directed` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.Cover.QuasiCompact` `Mathlib.AlgebraicGeometry.Cover.Sigma` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.IdealSheaf.Basic` `Mathlib.AlgebraicGeometry.IdealSheaf.Functorial` `Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme` `Mathlib.AlgebraicGeometry.LimitsOver` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.Morphisms.Descent` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.FlatDescent` `Mathlib.AlgebraicGeometry.Morphisms.FlatMono` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `Mathlib.AlgebraicGeometry.Morphisms.Immersion` `Mathlib.AlgebraicGeometry.Morphisms.Integral` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Morphisms.LocalClosure` `Mathlib.AlgebraicGeometry.Morphisms.LocalIso` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.Morphisms.Proper` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.Normalization` `Mathlib.AlgebraicGeometry.PointsPi` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.QuasiAffine` `Mathlib.AlgebraicGeometry.RationalMap` `Mathlib.AlgebraicGeometry.RelativeGluing` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.Pretopology` `Mathlib.AlgebraicGeometry.Sites.QuasiCompact` `Mathlib.AlgebraicGeometry.Sites.Representability` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.AlgebraicGeometry.ValuativeCriterion` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Combinatorics.Enumerative.Partition.GenFun` `Mathlib.Combinatorics.Enumerative.Partition.Glaisher` `Mathlib.FieldTheory.AbsoluteGaloisGroup` `Mathlib.FieldTheory.Galois.Abelian` `Mathlib.FieldTheory.Galois.Infinite` `Mathlib.FieldTheory.Galois.IsGaloisGroup` `Mathlib.FieldTheory.KrullTopology` `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.NumberTheory.Bernoulli` `Mathlib.NumberTheory.RamificationInertia.Galois` `Mathlib.RingTheory.AdicCompletion.Topology` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.IdealFilter.Topology` `Mathlib.RingTheory.MvPowerSeries.Evaluation` `Mathlib.RingTheory.MvPowerSeries.Expand` `Mathlib.RingTheory.MvPowerSeries.LinearTopology` `Mathlib.RingTheory.MvPowerSeries.PiTopology` `Mathlib.RingTheory.MvPowerSeries.Substitution` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.RingTheory.PowerSeries.Evaluation` `Mathlib.RingTheory.PowerSeries.Exp` `Mathlib.RingTheory.PowerSeries.Expand` `Mathlib.RingTheory.PowerSeries.PiTopology` `Mathlib.RingTheory.PowerSeries.Substitution` `Mathlib.Topology.Algebra.Group.SubmonoidClosure` `Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean` `Mathlib.Topology.Algebra.InfiniteSum.Ring` `Mathlib.Topology.Algebra.IsOpenUnits` `Mathlib.Topology.Algebra.Module.CharacterSpace` `Mathlib.Topology.Algebra.Module.Determinant` `Mathlib.Topology.Algebra.Module.Simple` `Mathlib.Topology.Algebra.Module.TransferInstance` `Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology` `Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete` `Mathlib.Topology.Algebra.Order.LiminfLimsup` `Mathlib.Topology.Algebra.TopologicallyNilpotent` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Topology.Algebra.Valued.WithZeroMulInt` `Mathlib.Topology.Covering.Quotient` `Mathlib.Topology.Instances.Matrix` `Mathlib.Topology.MetricSpace.Algebra` `Mathlib.Topology.Sheaves.CommRingCat`	2
84 files `Mathlib.Algebra.Category.ContinuousCohomology.Basic` `Mathlib.Algebra.Category.ModuleCat.Topology.Basic` `Mathlib.Algebra.Category.ModuleCat.Topology.Homology` `Mathlib.Analysis.CStarAlgebra.Module.Synonym` `Mathlib.Analysis.Fourier.Notation` `Mathlib.CategoryTheory.Galois.Equivalence` `Mathlib.CategoryTheory.Galois.EssSurj` `Mathlib.CategoryTheory.Galois.IsFundamentalgroup` `Mathlib.CategoryTheory.Galois.Topology` `Mathlib.Topology.Algebra.Algebra.Equiv` `Mathlib.Topology.Algebra.Algebra` `Mathlib.Topology.Algebra.ClopenNhdofOne` `Mathlib.Topology.Algebra.Equicontinuity` `Mathlib.Topology.Algebra.FilterBasis` `Mathlib.Topology.Algebra.Group.Basic` `Mathlib.Topology.Algebra.Group.ClosedSubgroup` `Mathlib.Topology.Algebra.Group.CompactOpen` `Mathlib.Topology.Algebra.Group.Compact` `Mathlib.Topology.Algebra.Group.GroupTopology` `Mathlib.Topology.Algebra.Group.OpenMapping` `Mathlib.Topology.Algebra.Group.Pointwise` `Mathlib.Topology.Algebra.Group.Quotient` `Mathlib.Topology.Algebra.Group.TopologicalAbelianization` `Mathlib.Topology.Algebra.GroupCompletion` `Mathlib.Topology.Algebra.InfiniteSum.Constructions` `Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion` `Mathlib.Topology.Algebra.InfiniteSum.Group` `Mathlib.Topology.Algebra.InfiniteSum.Module` `Mathlib.Topology.Algebra.InfiniteSum.NatInt` `Mathlib.Topology.Algebra.InfiniteSum.UniformOn` `Mathlib.Topology.Algebra.IsUniformGroup.Basic` `Mathlib.Topology.Algebra.IsUniformGroup.Constructions` `Mathlib.Topology.Algebra.IsUniformGroup.Defs` `Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup` `Mathlib.Topology.Algebra.IsUniformGroup.Order` `Mathlib.Topology.Algebra.LinearMapCompletion` `Mathlib.Topology.Algebra.LinearTopology` `Mathlib.Topology.Algebra.Localization` `Mathlib.Topology.Algebra.Module.Alternating.Basic` `Mathlib.Topology.Algebra.Module.Basic` `Mathlib.Topology.Algebra.Module.ClosedSubmodule` `Mathlib.Topology.Algebra.Module.Compact` `Mathlib.Topology.Algebra.Module.Equiv` `Mathlib.Topology.Algebra.Module.LinearMapPiProd` `Mathlib.Topology.Algebra.Module.LinearMap` `Mathlib.Topology.Algebra.Module.LinearPMap` `Mathlib.Topology.Algebra.Module.ModuleTopology` `Mathlib.Topology.Algebra.Module.Multilinear.Basic` `Mathlib.Topology.Algebra.Module.PerfectPairing` `Mathlib.Topology.Algebra.Module.Star` `Mathlib.Topology.Algebra.Module.WeakBilin` `Mathlib.Topology.Algebra.Module.WeakDual` `Mathlib.Topology.Algebra.MvPolynomial` `Mathlib.Topology.Algebra.NonUnitalAlgebra` `Mathlib.Topology.Algebra.NonUnitalStarAlgebra` `Mathlib.Topology.Algebra.Nonarchimedean.Bases` `Mathlib.Topology.Algebra.Nonarchimedean.Basic` `Mathlib.Topology.Algebra.Nonarchimedean.Completion` `Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected` `Mathlib.Topology.Algebra.OpenSubgroup` `Mathlib.Topology.Algebra.Order.UpperLower` `Mathlib.Topology.Algebra.ProperAction.AddTorsor` `Mathlib.Topology.Algebra.ProperAction.Basic` `Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace` `Mathlib.Topology.Algebra.Ring.Basic` `Mathlib.Topology.Algebra.Ring.Ideal` `Mathlib.Topology.Algebra.SeparationQuotient.Basic` `Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional` `Mathlib.Topology.Algebra.SeparationQuotient.Hom` `Mathlib.Topology.Algebra.SeparationQuotient.Section` `Mathlib.Topology.Algebra.StarSubalgebra` `Mathlib.Topology.Algebra.UniformConvergence` `Mathlib.Topology.Algebra.UniformFilterBasis` `Mathlib.Topology.Algebra.UniformMulAction` `Mathlib.Topology.Algebra.UniformRing` `Mathlib.Topology.Category.TopCommRingCat` `Mathlib.Topology.ContinuousMap.Algebra` `Mathlib.Topology.ContinuousMap.Lattice` `Mathlib.Topology.ContinuousMap.LocallyConstant` `Mathlib.Topology.ContinuousMap.Periodic` `Mathlib.Topology.ContinuousMap.Star` `Mathlib.Topology.Instances.TrivSqZeroExt` `Mathlib.Topology.UniformSpace.Matrix` `Mathlib.Topology.UniformSpace.ProdApproximation`	3
3 files `Mathlib.Analysis.Asymptotics.Lemmas` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter`	13
`Mathlib.Tactic.ComputeAsymptotics.Lemmas` (new file)	1446

Declarations diff

+ Filter.inv_nhdsGT
+ Filter.inv_nhdsLT
+ Filter.inv_nhdsNE
+ Filter.map_mul_left_nhdsGT
+ Filter.map_mul_left_nhdsLT
+ Filter.map_mul_left_nhdsNE
+ Filter.map_mul_right_nhdsGT
+ Filter.map_mul_right_nhdsLT
+ Filter.map_mul_right_nhdsNE
+ IsLittleO.of_tendsto_div_atBot
+ IsLittleO.of_tendsto_div_atTop
+ isBigOWith_of_div_tendsto_nhds
+ isBigOWith_of_tendsto_bot
+ isBigOWith_of_tendsto_top
+ isBigO_of_div_tendsto_atBot
+ isBigO_of_div_tendsto_atTop
+ isBigO_of_div_tendsto_nhds_of_ne_zero
+ isTheta_of_div_tendsto_nhds_ne_zero
+ tendsto_comp_inv_atBot_iff
+ tendsto_comp_inv_atTop_iff
+ tendsto_nhdsGT_of_tendsto_atTop
+ tendsto_nhdsGT_zero_of_comp_inv_tendsto_atTop
+ tendsto_nhdsLT_of_tendsto_atTop
+ tendsto_nhdsLT_zero_of_comp_inv_tendsto_atBot
+ tendsto_nhdsNE_of_tendsto_atTop
+ tendsto_nhdsNE_of_tendsto_atTop_nhds_of_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mathlib/Analysis/Asymptotics/Lemmas.lean

Mathlib/Tactic/ComputeAsymptotics/Lemmas.lean

j-loreaux

Thanks! I think we can move some of these directly into the library for convenience.

Mathlib/Tactic/ComputeAsymptotics/Lemmas.lean

mathlib4-dependent-issues-bot · 2026-01-29T18:00:18Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Analysis/Asymptotics): remove unnecessary hypothesis from isEquivalent_of_tendsto_one #34389~~
~~[Merged by Bors] - feat(Algebra/Order): multiplicative versions of lemmas on (pre)images of intervals under group operations #34561~~
By Dependent Issues (🤖). Happy coding!

mathlib-merge-conflicts · 2026-02-10T16:19:22Z

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

j-loreaux

Looks pretty good, thanks!

bors d+

Mathlib/Order/Filter/AtTopBot/Group.lean

Mathlib/Tactic/ComputeAsymptotics/Lemmas.lean

mathlib-bors · 2026-02-10T22:03:36Z

✌️ vasnesterov can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

vasnesterov · 2026-02-11T11:25:27Z

bors r+

…s to `Tendsto f atTop l` (#34403) Prove lemmas we use in `compute_asymptotics` to reduce various asymptotic goals to the case `Tendsto f atTop l`.

mathlib-bors · 2026-02-11T12:13:27Z

Pull request successfully merged into master.

Build succeeded:

…s to `Tendsto f atTop l` (leanprover-community#34403) Prove lemmas we use in `compute_asymptotics` to reduce various asymptotic goals to the case `Tendsto f atTop l`.

vasnesterov added 2 commits January 25, 2026 02:34

remove unnecessary hypothesis

ff3b590

lemmas wip

b2d6b02

vasnesterov added WIP Work in progress t-analysis Analysis (normed *, calculus) labels Jan 25, 2026

lemmas

2b47053

vasnesterov removed the WIP Work in progress label Jan 25, 2026

vasnesterov mentioned this pull request Jan 25, 2026

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

Open

12 tasks

vasnesterov changed the title ~~feat(Tactic/ComputeAsymptotics): Lemmas for converting different filters to atTop~~ feat(Tactic/ComputeAsymptotics): Lemmas for converting different goals to Tendsto f atTop l Jan 25, 2026

mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jan 25, 2026

Merge branch 'master' into compute_asymptotics_lemmas

bdc5e96

urkud reviewed Jan 26, 2026

View reviewed changes

Mathlib/Analysis/Asymptotics/Lemmas.lean Outdated Show resolved Hide resolved

urkud reviewed Jan 26, 2026

View reviewed changes

Mathlib/Tactic/ComputeAsymptotics/Lemmas.lean Outdated Show resolved Hide resolved

rename lemmas

7839e90

j-loreaux reviewed Jan 27, 2026

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 27, 2026

grunweg changed the title ~~feat(Tactic/ComputeAsymptotics): Lemmas for converting different goals to Tendsto f atTop l~~ feat(Tactic/ComputeAsymptotics): lemmas for converting different goals to Tendsto f atTop l Jan 27, 2026

vasnesterov added 6 commits January 29, 2026 00:14

some

25fccf2

multiplicative versions

5ca67ec

add header

69b5f33

remove variables

ea8c9ef

remove newlines

38e5ecc

Merge branch 'intervals_to_additive' into compute_asymptotics_lemmas

7e5eb4b

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 29, 2026

some

2cc459e

vasnesterov removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 29, 2026

vasnesterov added 3 commits January 29, 2026 14:33

remove unused arguments

92583ec

remove new line

d149a34

move

2cb074a

fix

a18e113

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 29, 2026

vasnesterov added 2 commits January 29, 2026 21:22

Merge branch 'master' into compute_asymptotics_lemmas

13578c9

update header

0f782cb

leanprover-community-bot-assistant assigned urkud Feb 2, 2026

IsBigOWith & IsTheta

01aea29

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 10, 2026

Merge branch 'master' into compute_asymptotics_lemmas

72baa4f

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 10, 2026

fix import

7084c14

j-loreaux reviewed Feb 10, 2026

View reviewed changes

Mathlib/Order/Filter/AtTopBot/Group.lean Outdated Show resolved Hide resolved

Mathlib/Order/Filter/AtTopBot/Group.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/ComputeAsymptotics/Lemmas.lean Outdated Show resolved Hide resolved

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 10, 2026

avoid change

b684815

mathlib-bors bot changed the title ~~feat(Tactic/ComputeAsymptotics): lemmas for converting different goals to Tendsto f atTop l~~ [Merged by Bors] - feat(Tactic/ComputeAsymptotics): lemmas for converting different goals to Tendsto f atTop l Feb 11, 2026

mathlib-bors bot closed this Feb 11, 2026

Conversation

vasnesterov commented Jan 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary f7ee1844c2

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Jan 29, 2026

Uh oh!

mathlib-merge-conflicts bot commented Feb 10, 2026

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Feb 10, 2026

Uh oh!

vasnesterov commented Feb 11, 2026

Uh oh!

mathlib-bors bot commented Feb 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

vasnesterov commented Jan 25, 2026 •

edited

Loading

github-actions bot commented Jan 25, 2026 •

edited

Loading