[Merged by Bors] - feat: Density of a finset#11243
[Merged by Bors] - feat: Density of a finset#11243YaelDillies wants to merge 5 commits intomasterfrom
Conversation
|
See also |
5628d4b to
6588c21
Compare
Nice observation! Will do so in a later PR.
Maybe in a distant future but right now I don't need it. |
The density of a finite set in an ambient group is a quantity of great interest in combinatorics. This PR defines `Finset.dens s` for `s : Finset α` as the size of `s` divided by the size of `α`, with value in any semifield. The API lemmas are copied from `Finset.card` (but not all `Finset.card` lemmas are sensible `Finset.dens` lemmas). From LeanAPAP
012fb4f to
68e0f47
Compare
PR summary 8241efc7a4
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Tactic.Positivity.Finset | 488 | 538 | +50 (+10.25%) |
Import changes for all files
| Files | Import difference |
|---|---|
3 filesMathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Tactic |
1 |
Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite |
6 |
Mathlib.Tactic.Positivity.Finset |
50 |
Mathlib.Data.Finset.Density |
537 |
Declarations diff
+ dens
+ dens_cons
+ dens_disjUnion
+ dens_empty
+ dens_eq_card_div_card
+ dens_eq_one
+ dens_eq_zero
+ dens_filter_add_dens_filter_not_eq_dens
+ dens_inter_add_dens_sdiff
+ dens_inter_add_dens_union
+ dens_le_dens
+ dens_le_dens_sdiff_add_dens
+ dens_lt_dens
+ dens_map_le
+ dens_mono
+ dens_ne_one
+ dens_ne_zero
+ dens_pos
+ dens_sdiff
+ dens_sdiff_add_dens
+ dens_sdiff_add_dens_eq_dens
+ dens_sdiff_add_dens_inter
+ dens_sdiff_comm
+ dens_singleton
+ dens_strictMono
+ dens_union_add_dens_inter
+ dens_union_le
+ dens_union_of_disjoint
+ dens_univ
+ evalFinsetDens
+ le_dens_sdiff
+ they
++ ⟨_,
You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
Feel free to put on the maintainer queue regardless of your response to my comment below, as long as you're convinced.
The density of a finite set in an ambient group is a quantity of great interest in combinatorics. This PR defines `Finset.dens s` for `s : Finset α` as the size of `s` divided by the size of `α`, with value in any semifield. The API lemmas are copied from `Finset.card` (but not all `Finset.card` lemmas are sensible `Finset.dens` lemmas). From LeanAPAP
|
This PR was included in a batch that was canceled, it will be automatically retried |
The density of a finite set in an ambient group is a quantity of great interest in combinatorics. This PR defines `Finset.dens s` for `s : Finset α` as the size of `s` divided by the size of `α`, with value in any semifield. The API lemmas are copied from `Finset.card` (but not all `Finset.card` lemmas are sensible `Finset.dens` lemmas). From LeanAPAP
|
Pull request successfully merged into master. Build succeeded: |
The density of a finite set in an ambient group is a quantity of great interest in combinatorics.
This PR defines
Finset.dens sfors : Finset αas the size ofsdivided by the size ofα, with value in any semifield.The API lemmas are copied from
Finset.card(but not allFinset.cardlemmas are sensibleFinset.denslemmas).From LeanAPAP