feat(information_theory/linear_code): Define linear codes #16774
Conversation
BoltonBailey
changed the title
BoltonBailey
added
the
awaiting-CI
|
|
||
| * `linear_code 𝓓 F`: The type of linear codes with domain `𝓓` over field `F` |
There was a problem hiding this comment.
| * `linear_code 𝓓 F`: The type of linear codes with domain `𝓓` over field `F` | |
| * `linear_code 𝓓 F`: The type of linear codes with domain `𝓓` over field `F` |
| A linear error-correcting code, defined as a subspace of the vector space of functions from a | ||
| domain into a field. | ||
| -/ | ||
| def linear_code (𝓓 F : Type) [fintype 𝓓] [field F] := submodule F ( 𝓓 -> F ) |
There was a problem hiding this comment.
The fintype assumption is unused.
There was a problem hiding this comment.
Which incidentally is to be expected - this is a problem I ran into. It's actually not really necessary that this be finite....
There was a problem hiding this comment.
Given that you're interested in matrices associated with the code, maybe it would be best to go with domain fin n
There was a problem hiding this comment.
Not for the general definition.
There was a problem hiding this comment.
Incidentally, you should use hamm (𝓓 -> F) as the type of the vectors: this is 𝓓 -> F equipped with the hamming norm as a metric.
There was a problem hiding this comment.
Yeah I tried that but module F (hamming (λ (d : 𝓓), F)) failed to synthesize, presumably at some point I should go back and switch that.
There was a problem hiding this comment.
Hmm - it shouldn't have done, in theory. I would be grateful if you could try and replicate the issue in case it needs a patch.
There was a problem hiding this comment.
Maybe one should not hardcode hamm as the metric. Different types of codes use different metrics. E.g. your code may live in a matrix space, with distance the rank distance, i.e. dist(A,B)=rank(A-B).
There was a problem hiding this comment.
Yes, this is another reason I have hesitated before defining codes. I think it does want to be generalised ideally. It might want to be specific to integer-valued distances but this might not actually be necessary.
| def length (C : linear_code 𝓓 F) : ℕ := fintype.card 𝓓 | ||
|
|
||
| /-- The set of all valid codewords -/ | ||
| def codewords (C : linear_code 𝓓 F) := C.carrier |
There was a problem hiding this comment.
Probably this should be a set_like instance instead.
| hamming distance of 0 from any nonzero element of the code. | ||
| -/ | ||
| noncomputable def distance [decidable_eq F] (C : linear_code 𝓓 F) : ℕ := | ||
| Inf (set.image (λ w : hamming (λ i : 𝓓, F), hamming_dist w 0) (C.codewords \ {0})) |
There was a problem hiding this comment.
Please use the '' notation You can also use nat.find maybe.
There was a problem hiding this comment.
I've been working on this for a little while (actually longer than I probably should have been). Well done for submitting it. I'm not sure this is the right approach to the minimum distance, however - at the very least, there's a number of theorems you'll want to show are true about it. I have a branch called infsep where I've been trying to define this concept rigourously.
| Inf (set.image (λ w : hamming (λ i : 𝓓, F), hamming_dist w 0) (C.codewords \ {0})) | ||
|
|
||
| /-- The proportion of the code dimension to the size of the code -/ | ||
| noncomputable def rate (C : linear_code 𝓓 F) : ℚ := rat.mk C.dimension C.length |
There was a problem hiding this comment.
rat.mk has a better name in informal maths 😉
| noncomputable def rate (C : linear_code 𝓓 F) : ℚ := rat.mk C.dimension C.length | |
| noncomputable def rate (C : linear_code 𝓓 F) : ℚ := C.dimension / C.length |
| intros a b ha hb, | ||
| rw set.mem_set_of at ha hb ⊢, | ||
| rcases ha with ⟨pa, hap⟩, | ||
| rcases hb with ⟨pb, hbp⟩, |
There was a problem hiding this comment.
| intros a b ha hb, | |
| rw set.mem_set_of at ha hb ⊢, | |
| rcases ha with ⟨pa, hap⟩, | |
| rcases hb with ⟨pb, hbp⟩, | |
| rintro a b ⟨pa, hap⟩ ⟨pb, hbp⟩, |
|
I feel a bit stupid because I've written versions of this same file a bunch of times in the last few months, I never submitted it, and now you actually did it - well done. However: my suspicion is that you might run into the same issues I did. What this file lacks is many or any theorems. You're doing a lot of defining things - but every definition comes with a cost. What I want to see is some theorems proving (not necessarily complicated!) facts about these objects. In addition - it doesn't make sense to me to define linear codes without first defining block codes, which was a sticking point for me. You're not really using the linearity that much in what you've done so far. I would expect to see some mention of generating matrices and parity check matrices... |
|
I would be interested to see if you could base this off my |
mathlib-dependent-issues-bot
added
blocked-by-other-PR
|
This PR/issue depends on: |
| /-- The repetition code, where all symbols in each codeword are the same. This is equivalent to a | ||
| Reed-Solomon code with max degree 0 -/ | ||
| def repetition : linear_code 𝓓 F := | ||
| { carrier := {w | ∃ f : F, w = (λ x, f)}, |
There was a problem hiding this comment.
This would be much easier to prove as something like
linear_map.range { to_fun := function.const, map_add' := pi.const_add }
| field. | ||
| -/ | ||
| def reed_solomon (k : ℕ) (D : finset F) : linear_code D F := | ||
| { carrier := {w | ∃ p : polynomial F, p.nat_degree ≤ k ∧ w = (λ x, polynomial.eval x p)}, |
There was a problem hiding this comment.
You should be able to write this as the submodule.image of eval on the polynomials of degree-less- than-k.
semorrison
added
the
too-late
Add linear codes and defines the Reed-Solomon code.