Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat(1000): fill in more entries #20470

Merged
merged 3 commits into from
Jan 6, 2025
Merged

feat(1000): fill in more entries #20470

merged 3 commits into from
Jan 6, 2025

Conversation

YaelDillies
Copy link
Collaborator

Open in Gitpod

@YaelDillies YaelDillies added the documentation Improvements or additions to documentation label Jan 4, 2025
@github-actions GitHub Actions
Copy link

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

PR summary 9c682696eb

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ _root_.IsAntichain.sperner
- IsAntichain.sperner

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

RemyDegenne
RemyDegenne reviewed Jan 4, 2025
View reviewed changes
@fpvandoorn
Copy link
Member

Thanks!

@fpvandoorn fpvandoorn merged commit 9ab795a into master Jan 6, 2025
12 checks passed
@mathlib-bors mathlib-bors bot deleted the more_1000_info branch January 6, 2025 15:20
@fpvandoorn
Copy link
Member

Oops, I intended to bors merge this. I've been on a break for too long... It should still be fine like this.

Julian added a commit that referenced this pull request Jan 6, 2025
@Julian
Merge remote-tracking branch 'origin/master' into nat-ideal-eq-top
ca07f7f 
* origin/master: (189 commits)
  chore(Algebra): make more names consistent (#20449)
  feat: Polynomial FLT (#18882)
  feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty (#20457)
  fix: linkfix in 100.yaml (#20517)
  feat(1000): fill in more entries (#20470)
  feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` (#16769)
  feat(ContinuousMultilinearMap): add lemmas about `.prod` (#20462)
  feat(RingTheory): classification of etale algebras over fields (#20324)
  fix: Allow multiple builds on staging branch (#20515)
  feat(CategoryTheory/Shift/Adjunction): properties of `Adjunction.CommShift` (#20337)
  chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower (#19863)
  chore(Topology/UniformSpace/Completion): make coe' argument implicit (#20514)
  refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in `AddCommGrp` (#20474)
  feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544)
  chore(RingTheory/Finiteness): rename Module.Finite.out (#20506)
  refactor(CategoryTheory/Limits/Preserves/Ulift): simplify the proof that the universe lifting functor for types preserves all colimits (#20508)
  feat(CategoryTheory): products in the category of Ind-objects (#20507)
  chore: remove >9 month old deprecations (#20505)
  chore(FieldTheory/Galois): small cleanup (#20217)
  chore(LinearIndependent): generalize to semirings (#20480)
  chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500)
  chore: replace `aesop` with `simp` where possible (#20483)
  chore(1000): remove nonexistent fields (#20493)
  chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490)
  feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458)
  feat: a conditional kernel is almost everywhere a probability measure (#20430)
  feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304)
  feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479)
  chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492)
  feat(FaaDiBruno): derive `DecidableEq` (#20482)
  chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413)
  chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351)
  chore(MvPolynomial/Localization): golf using TensorProduct (#20309)
  chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277)
  chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259)
  feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091)
  fix: Stop cancelling builds of master (#20435)
  chore: update Mathlib dependencies 2025-01-05 (#20485)
  feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933)
  chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464)
  chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478)
  feat: shorthand lemmas for the L1 norm (#20383)
  chore: remove unnecessary adaptation notes (#20467)
  chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473)
  chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888)
  feat(Algebra): more on `OrthogonalIdempotents` (#18195)
  feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468)
  feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190)
  feat(Algebra/Lie): add Lie's theorem (#13480)
  chore(RingTheory/Generators): make algebra instance a def (#14265)
  ...
kex-y
kex-y reviewed Jan 10, 2025
View reviewed changes
docs/1000.yaml
@@ -3605,6 +3732,9 @@ Q10942247:

Q11352023:
title: Vitali convergence theorem
decl: MeasureTheory.tendstoInMeasure_iff_tendsto_Lp
author: Igor Khavkine
Copy link
Member

Choose a reason for hiding this comment

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

I formalized Vitali convergence in leanprover-community/mathlib3#12408 ...

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

but only the finite measure version, right? Maybe we can reference both versions

Copy link
Member

Choose a reason for hiding this comment

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

My bad, I did not realize the version using unif_tight is also called Vitali convergence. In that case the authorship is accurate and I'm happy to keep it as it is.

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

@RemyDegenne RemyDegenne RemyDegenne left review comments

@kex-y kex-y kex-y left review comments

Assignees
No one assigned
Labels
documentation Improvements or additions to documentation
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@YaelDillies @fpvandoorn @RemyDegenne @kex-y