feat(Combinatorics/Colex): binary expansions give the colexicographic order on Finset Nat
#12346
Conversation
apnelson1
added
the
awaiting-review
There was a problem hiding this comment.
The definition
bitSetcould be argued to fit inNat/BitsorNat/Digits, but both are quite far back in the import hierarchy compared toFinset, and the proof of bijectivity uses the machinery inColex.
According to #11757, they shouldn't be, so I believe you could put that material there, or at least in a separate file since it really sticks out from the rest of Combinatorics.Colex.
Mathlib/Combinatorics/Colex.lean
Outdated
|
|
||
| /-- The function which maps the natural number `∑ i ∈ s, 2^i` to the Finset `s`. | ||
| This could also be defined using `Nat.bits`, but it seems easier to avoid the `List` api. -/ | ||
| def Nat.bitSet (n : ℕ) : Finset ℕ := by |
There was a problem hiding this comment.
| def Nat.bitSet (n : ℕ) : Finset ℕ := by | |
| def Nat.bitsFinset (n : ℕ) : Finset ℕ := by |
is more accurate maybe?
There was a problem hiding this comment.
Possibly, but it isn't so nice-looking mathematically, and I think there is little danger of ambiguity. I'll let others weigh in.
There was a problem hiding this comment.
You're right that it sticks out. I've moved it to a separate file - importing |
YaelDillies
added
awaiting-zulip
and removed
awaiting-review
Mathlib/Data/Nat/Bitset.lean
Outdated
| induction' n using binaryRec with b _ s | ||
| · exact ∅ | ||
| cases b | ||
| · exact image (· + 1) s |
There was a problem hiding this comment.
Can you use map here instead? It will be faster and have nicer defeqs. Same for cons instead of insert below.
There was a problem hiding this comment.
edit : never mind
| variable {a n : ℕ} {s : Finset ℕ} | ||
|
|
||
| /-- The function which maps the natural number `∑ i in s, 2^i` to the Finset `s`. -/ | ||
| def bitIndices (n : ℕ) : Finset ℕ := by |
There was a problem hiding this comment.
Should this be a (sorted) list instead of a finset? Nothing about the name suggests that it should be a finset. See Nat.factors for a similar case of using a list instead.
There was a problem hiding this comment.
In the context of colex, it should be a finset. But that doesn't mean we can't construct it as a list originally.
|
Coming here from PR triage: is this PR still blocked on a zulip decision? |
There was a problem hiding this comment.
No, I didn't pay attention but 69c62a1 changed the PR to follow the convention explained in https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2312346.20Colexicographic.20order.20on.20.60Finset.20Nat.60.
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Peter Nelson | ||
| -/ | ||
| import Mathlib.Combinatorics.Colex |
There was a problem hiding this comment.
I think Combinatorics.Colex should import Data.Nat.BitIndices, not the other way around. Can you turn the imports around?
YaelDillies
added
awaiting-author
This PR fills in a todo in
Combinatorics/Colexby providing the natural order isomorphism betweenNatandColex Natthat maps eachnto the set of indices of ones in the binary expansion ofn.We define
bitSet nto be this 'finset of bits' corresponding ton, and prove a few API lemmas for it, before defining the equivalence. The definitionbitSetcould be argued to fit inNat/BitsorNat/Digits, but both are quite far back in the import hierarchy compared toFinset, and the proof of bijectivity uses the machinery inColex.