[Merged by Bors] - feat: The diagonal of a finset #13899
Conversation
PR summary bd289da70a
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.Finset.Pi | 411 | 412 | +1 (+0.24%) |
| Mathlib.Data.Fintype.Pi | 418 | 419 | +1 (+0.24%) |
Import changes for all files
| Files | Import difference |
|---|---|
4 filesMathlib.Data.Fin.Tuple.Finset Mathlib.Data.Finset.Pi Mathlib.Data.Fintype.Pi Mathlib.Data.Fintype.Vector |
1 |
Declarations diff
+ card_piDiag
+ mem_piDiag
+ piDiag
+ piDiag_subset_piFinset
+ piFinset_filter_const
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>
Mathlib/Data/Fintype/Pi.lean
Outdated
| variable {ι : Type*} [DecidableEq (ι → α)] {s : Finset α} {f : ι → α} | ||
|
|
||
| /-- The diagonal of a finset `s : Finset α` as a finset of functions `ι → α`. -/ | ||
| def piDiag (s : Finset α) (ι : Type*) [DecidableEq (ι → α)] : Finset (ι → α) := s.image (const ι) |
There was a problem hiding this comment.
Subtly, no: If \iota is empty, then const \iota is not injective. Of course in that case the finset is obvious to construct, but I can't case on whether \iota is empty or not (unless I assume Decidable (IsEmpty \iota) which is.. unorthodox)
There was a problem hiding this comment.
Does the empty case make any sense in your application?
There was a problem hiding this comment.
It would be kind of strange as my application is \iota := Fin n and I would have to rule out n = 0 explicitly. Not the end of the world, though.
Mathlib/Data/Finset/Pi.lean
Outdated
|
|
||
| variable {ι : Type*} [DecidableEq (ι → α)] {s : Finset α} {f : ι → α} | ||
|
|
||
| /-- The diagonal of a finset `s : Finset α` as a finset of functions `ι → α`. -/ |
There was a problem hiding this comment.
Maybe this is just my ignorance, but I'm not sure what a diagonal is after reading this comment
There was a problem hiding this comment.
Perhaps foreshadow what this is for?
There was a problem hiding this comment.
I'm not sure my use case is a good fit for the docstring. It is used inside a proof of Almost Periodicity, where we are interested in tuples x and y differing by a constant, and we are interested in tuples because we can use a concentration inequality to approximate some random variable X by an average of uniform variables x 0, ..., x (n - 1) valued in some set.
You can see it for yourself here: https://github.com/search?q=repo%3AYaelDillies%2FLeanAPAP%20wideDiag&type=code (it's currently called wideDiag in APAP)
|
|
||
| /-- The diagonal of a finset `s : Finset α` as a finset of functions `ι → α`, namely the set of | ||
| constant functions valued in `s`. -/ | ||
| def piDiag (s : Finset α) (ι : Type*) [DecidableEq (ι → α)] : Finset (ι → α) := s.image (const ι) |
There was a problem hiding this comment.
Would constFnsWithin be better? I think a niche notion like this can afford to have a long name, and should have a name that is clear.
There was a problem hiding this comment.
I see your point, but it is completely analogous to Finset.diag, except for ι → α rather than α × α. I think this justifies the current name (and points to the fact that we might want the ι →₀ α version in the future, which is not something your naming scheme would allow)
From LeanAPAP
long line
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
|
!bench |
|
Here are the benchmark results for commit bd289da. |
|
Thanks! bors merge |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
From LeanAPAP