Skip to content

[Merged by Bors] - feat(Asymptotics): prove IsLittleOTVS.add#20578

Closed
urkud wants to merge 36 commits intomasterfrom
YK-oTVS-add
Closed

[Merged by Bors] - feat(Asymptotics): prove IsLittleOTVS.add#20578
urkud wants to merge 36 commits intomasterfrom
YK-oTVS-add

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Jan 8, 2025 •
edited by sgouezel
Loading

@urkud urkud added the t-analysis Analysis (normed *, calculus) label Jan 8, 2025
@urkud urkud requested a review from eric-wieser January 8, 2025 19:08
@urkud urkud marked this pull request as draft January 8, 2025 19:08
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 8, 2025 •
edited
Loading

messageFile.md

eric-wieser
eric-wieser reviewed Jan 8, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Jan 8, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Jan 8, 2025
View reviewed changes
@mathlib4-dependent-issues-bot 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 9, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 9, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 10, 2025
@mathlib4-dependent-issues-bot 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 13, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Jan 13, 2025

This PR/issue depends on:

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Jan 13, 2025

Is this ready to leave the draft state now?

@urkud urkud marked this pull request as ready for review January 14, 2025 09:34
eric-wieser
eric-wieser reviewed Jan 15, 2025
View reviewed changes
@urkud
Copy link
Copy Markdown
Member Author

urkud commented Jan 28, 2025

Co-authored by 2 maintainers who agree that it's ready to be merged, so
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 28, 2025

🚀 Pull request has been placed on the maintainer queue by urkud.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 28, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 28, 2025

PR summary 0b6c932b8d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Eventually.exists_mem_basis_of_smallSets
+ Eventually.exists_mem_of_smallSets
+ Filter.HasBasis.mul_self
+ Frequently.smallSets_of_forall_mem_basis
+ IsLittleOTVS.add
+ egauge_add_add_le

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).

jcommelin
jcommelin reviewed Jan 28, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 28, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 28, 2025
@urkud @eric-wieser
feat(Asymptotics): prove IsLittleOTVS.add (#20578)
eff2ae8 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 28, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Asymptotics): prove IsLittleOTVS.add [Merged by Bors] - feat(Asymptotics): prove IsLittleOTVS.add Jan 28, 2025
@mathlib-bors mathlib-bors bot closed this Jan 28, 2025
@mathlib-bors mathlib-bors bot deleted the YK-oTVS-add branch January 28, 2025 07:53
Julian added a commit that referenced this pull request Jan 28, 2025
@Julian
Merge remote-tracking branch 'origin/master' into polynomial-sequences
c572510 
* origin/master: (294 commits)
  feat: equalizers and coequalizers in the category of ind-objects (#21139)
  doc: turn more links to Stacks into `@[stacks]` tags (#21135)
  feat(Asymptotics): prove `IsLittleOTVS.add` (#20578)
  feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062)
  chore: import Std in Mathlib.lean (#21126)
  feat(Data/Matroid/Circuit): fundamental circuits and extensionality  (#21145)
  feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140)
  feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109)
  feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042)
  doc: fixed notation error in customizing category composition (#21132)
  feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143)
  chore(SupIndep): speedup the `Decidable` instance (#21114)
  fix(CI): use `Elab.async=false` for late importers workflow (#21147)
  feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687)
  feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921)
  feat(Algebra): `Pi.single_induction` (#21141)
  chore(BigOperators/Fin): golf a proof (#21131)
  feat: generalize tangent cone lemmas to TVS (#20859)
  feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136)
  refactor: unapply matrix lemmas (#21091)
  chore(Algebra/Category): `erw` -> `rw` (#21130)
  feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128)
  feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125)
  feat: PSum of finite sorts is finite (#20285)
  feat: inequality on the integral of a convex function of a RN derivative (#21093)
  feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058)
  chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317)
  feat: a `RelHom` preserves directedness (#20080)
  feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677)
  chore(Data/Matrix/PEquiv): clean up names (#21108)
  feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815)
  feat: define Descriptive.Tree (#18763)
  chore(Data/Complex/Exponential): split trig functions to new file (#21075)
  feat(Logic/IsEmpty/Relator): empty on sides (#20319)
  feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121)
  feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661)
  feat(RingTheory/LaurentSeries): add algebraEquiv (#21004)
  chore(SetTheory/Game/Impartial): golf two proofs (#21074)
  feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047)
  feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023)
  feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994)
  feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970)
  feat(RingTheory/Artinian): `IsUnit a` iff `a ∈ R⁰` for an artinian ring `R` (#21084)
  feat: separating set in the category of ind-objects (#21082)
  feat: derivWithin lemmas (#21092)
  chore(Fintype): golf a proof (#21113)
  chore: golf using `funext₂` (#21106)
  chore(Algebra/Group/Submonoid/Operations): move instances to new file (#21067)
  doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations (#21101)
  doc(ComputeDegree): typos (#21095)
  ...
Julian added a commit that referenced this pull request Feb 1, 2025
@Julian
Merge branch 'polynomial-sequences' into bhargava-factorial
3dacf71 
* polynomial-sequences: (308 commits)
  Use the lemma we already added.
  Minor reordering.
  This is true even for the trivial ring.
  Also add the lt versions and the other inj lemma.
  Also add the basis ne versions.
  This seems also like it should be simp.
  Back to sorry free.
  And the natDegree version.
  feat: equalizers and coequalizers in the category of ind-objects (#21139)
  doc: turn more links to Stacks into `@[stacks]` tags (#21135)
  feat(Asymptotics): prove `IsLittleOTVS.add` (#20578)
  feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062)
  chore: import Std in Mathlib.lean (#21126)
  feat(Data/Matroid/Circuit): fundamental circuits and extensionality  (#21145)
  feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140)
  feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109)
  feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042)
  doc: fixed notation error in customizing category composition (#21132)
  feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143)
  chore(SupIndep): speedup the `Decidable` instance (#21114)
  fix(CI): use `Elab.async=false` for late importers workflow (#21147)
  feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687)
  feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921)
  feat(Algebra): `Pi.single_induction` (#21141)
  chore(BigOperators/Fin): golf a proof (#21131)
  feat: generalize tangent cone lemmas to TVS (#20859)
  feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136)
  refactor: unapply matrix lemmas (#21091)
  chore(Algebra/Category): `erw` -> `rw` (#21130)
  feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128)
  feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125)
  feat: PSum of finite sorts is finite (#20285)
  feat: inequality on the integral of a convex function of a RN derivative (#21093)
  feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058)
  chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317)
  feat: a `RelHom` preserves directedness (#20080)
  feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677)
  chore(Data/Matrix/PEquiv): clean up names (#21108)
  feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815)
  feat: define Descriptive.Tree (#18763)
  chore(Data/Complex/Exponential): split trig functions to new file (#21075)
  feat(Logic/IsEmpty/Relator): empty on sides (#20319)
  feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121)
  feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661)
  feat(RingTheory/LaurentSeries): add algebraEquiv (#21004)
  chore(SetTheory/Game/Impartial): golf two proofs (#21074)
  feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047)
  feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023)
  feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994)
  feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

Derivatives in Topological Vector Spaces
Status: Done

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@urkud @mathlib4-dependent-issues-bot @eric-wieser @jcommelin @leanprover-community-bot-assistant