Zulip Chat Archive
Stream: new members
Topic: Buiding a Coding Theory Library
Allan Li (Jan 18 2024 at 08:32):
I am new to lean4 and am starting a project on building a coding theory library. I am having trouble on defining the distance of a code, which is . Here is my code:
import Mathlib.Logic.Equiv.Fin
import Mathlib.Analysis.SpecificLimits.Normed
import Mathlib.InformationTheory.Hamming
import Mathlib.Data.Finset.Basic
import Mathlib.Init.Set
open Set Filter Asymptotics Finset
namespace CodingTheory
variable {𝔽 : Type*} [Field 𝔽] [Fintype 𝔽] [DecidableEq 𝔽]
variable {α : Type} [Fintype 𝔽] [DecidableEq α]
variable {n k : ℕ}
/-- A type that represents the set of symbols in the code -/
abbrev Alphabet := Set α
/-- An element of 𝔽ⁿ. -/
abbrev Codeword (n : ℕ) (𝔽 : Type*) [Field 𝔽] [Fintype 𝔽] [DecidableEq 𝔽] := Fin n → 𝔽
/-- Code `Code n 𝔽` is a subset of 𝔽ⁿ. -/
abbrev Code (n : ℕ) (𝔽 : Type*) [Field 𝔽] [Fintype 𝔽] [DecidableEq 𝔽] := Finset (Codeword n 𝔽)
def hamming_distance (c1 c2 : Codeword n 𝔽) : ℕ :=
hammingDist c1 c2
/-- This gives me an error. -/
def distance {n : ℕ} (C : Code n 𝔽) : ℕ :=
Finset.min' {d : Fin n | ∃ x ∈ C, ∃ y ∈ C, x ≠ y ∧ hamming_distance x y = d}
I am happy to take any comments/suggestions on the code.
ohhaimark (Jan 18 2024 at 10:10):
Disclaimer, I'm a mathlib noob but:
{d : Fin n | ∃ x ∈ C, ∃ y ∈ C, x ≠ y ∧ hamming_distance x y = d}
is a Set, not a FinSet. I think you can use Finset.range
and Finset.filter
to get a finset of what you want.
Another problem is that Finset.min' takes two arguments, a finset and a proof that it is non-empty, but I think if n is 0, there is only one codeword, but you need two distinct codewords for an element of your FinSet and it can therefore be empty.
Ruben Van de Velde (Jan 18 2024 at 10:16):
^ I can confirm this is correct :)
Martin Dvořák (Jan 18 2024 at 10:17):
I don't think d : Fin n
is a good idea.
Martin Dvořák (Jan 18 2024 at 10:21):
Not a direct answer to your question, but I think this definition might be useful:
def separated {n : ℕ} (C : Code n 𝔽) (d : ℕ) : Prop :=
∀ x ∈ C, ∀ y ∈ C, x ≠ y → hamming_distance x y ≥ d
Martin Dvořák (Jan 18 2024 at 10:23):
My last comment: I don't see what Alphabet
should do in your code.
ohhaimark (Jan 18 2024 at 11:12):
To elaborate, perhaps unnecesarily, separated C 0
is always true since x ≥ 0
is always true and since ℕ is well founded, you can find the minimum d such that separated C d
. I think that'll translate fairly straightforwardly in mathlib.
Martin Dvořák (Jan 18 2024 at 11:22):
The interesting question is the maximum d
such that...
ohhaimark (Jan 18 2024 at 11:24):
Oh. I should refrain from commenting with my airheadedness
Bolton Bailey (Jan 18 2024 at 11:26):
If you are interested in coding theory you might be interested in talking to @Wrenna Robson
Wrenna Robson (Jan 18 2024 at 11:27):
Hi. @Allan Li we already have the hamming metric defined
Wrenna Robson (Jan 18 2024 at 11:27):
We also have a construct called infsup (I think) which is designed to be used for exactly this
Bolton Bailey (Jan 18 2024 at 11:27):
Yeah, I was going to say, if you want spoilers, you can see how mathlib defines the hamming distance at docs#hammingDist
Wrenna Robson (Jan 18 2024 at 11:28):
Wrenna Robson (Jan 18 2024 at 11:29):
However yeah I had a go at defining linear codes a year or two ago and I never really got anywhere with it. I know Dan Bernstein has done some formalisation in this area too but his work hasn't made it to Mathlib in any form.
Wrenna Robson (Jan 18 2024 at 11:29):
Ah I see you have already imported the hamming distance file
Wrenna Robson (Jan 18 2024 at 11:30):
What you want to do is define Codeword as Hamming (Fin n -> alpha)
Wrenna Robson (Jan 18 2024 at 11:31):
And then the hamming distance of a set of codewords is given by s.infsep
Wrenna Robson (Jan 18 2024 at 11:31):
(because that's the ambient metric on the space)
Wrenna Robson (Jan 18 2024 at 11:32):
The design intent was always to use this for codes but I never got round to putting infsep and hamming together!
Wrenna Robson (Jan 18 2024 at 11:36):
But yeah above people are trying to go down the path I already went down when I made infsep. You don't need to do this again!
Wrenna Robson (Jan 18 2024 at 11:37):
The only thing we could ARGUABLY do with is a definition of Finset.infsep but I think we decided that wasn't strictly necessary. You'd want it if you wanted a computable version I guess.
Wrenna Robson (Jan 18 2024 at 11:38):
What's interesting actually is that the hamming distance has a very well-behaved infsep even not on final steps because it takes integer values. I don't think we ever worked out quite how to formalise that property.
Wrenna Robson (Jan 18 2024 at 11:42):
By well behaved I mean "a set is non-trivial if and only if its infsep is positive" - that's true for finite sets, and we have that, but what we don't have is a notion of, I guess, a "discrete metric" (in the sense of a metric that gives rise to the discrete topology, rather than the usual sense of discrete metric).
Wrenna Robson (Jan 18 2024 at 11:43):
Or I guess, specifically, a metric where non-equal things have some minimum distance.
Wrenna Robson (Jan 18 2024 at 12:05):
So actually it's univ.infsep > 0 isn't it
Wrenna Robson (Jan 18 2024 at 12:09):
Which is somewhat the relatively discrete stuff in there, but it's very limited and could do with extending.
Wrenna Robson (Jan 18 2024 at 12:13):
Also I feel like maybe that ought to be "uniformly discrete"
Wrenna Robson (Jan 18 2024 at 12:16):
Based on https://en.m.wikipedia.org/wiki/Delone_set
Wrenna Robson (Jan 18 2024 at 12:17):
I think I got as far as suggesting that we ought to have a notion of uniformly discrete metric spaces but no further.
Wrenna Robson (Jan 18 2024 at 12:18):
I still think this!
Wrenna Robson (Jan 18 2024 at 12:22):
We should define UniformlyDiscrete and RelativelyDense as predicates on sets with a metric, and then we could also define Delone, and then we could define a UniformlyDiscrete(E)Metric as a metric for which univ is a UniformlyDiscrete set.
Wrenna Robson (Jan 18 2024 at 12:22):
All of which would help with coding theory but isn't directly related to it, but this was kind of what I found: you end up having to do a lot of stuff in specific that really you want to define in general and then be specific about.
Wrenna Robson (Jan 18 2024 at 12:26):
We might also want to define covering radius and packing radius which are related but not the same.
Wrenna Robson (Jan 18 2024 at 12:26):
It all needs a plan, basically, and I was only one person working on my own so it was hard to get any engagement with it.
Wrenna Robson (Jan 22 2024 at 08:45):
@Allan Li i would be interested to help out if and when you take this further
Allan Li (Jan 22 2024 at 08:49):
@Wrenna Robson I am thinking about taking this project further. I have already set up the blueprint and documentation for the project https://shilun-allan-li.github.io/tcslib/ I am thinking about following lectures notes on coding theory and implementing the blueprint of the theorems first.
Wrenna Robson (Jan 22 2024 at 08:58):
Sounds great.
Wrenna Robson (Jan 22 2024 at 09:15):
Was the above useful?
Allan Li (Jan 22 2024 at 09:15):
Yeah, thanks for the advice
Wrenna Robson (Jan 22 2024 at 09:19):
I think the definition of code there is as good as any. For what it's worth I think it might be good to have this stuff in mathlib but I guess it could be downstream.
Allan Li (Jan 22 2024 at 09:28):
I'm creating a new library since I'm also trying to formalize other TCS results (for example complexity theory). I'm note sure if these results would fit into mathlib
Edward van de Meent (Feb 09 2024 at 23:00):
i tried to replicate these definitions, while extending it to define all Codes instead of just linear codes and got a decent way, even defining the minimal distance, dimension, and rate of a code.
i'd like to also formalise the hamming bound and possibly even prove it, but i'm having a bit of trouble integrating with the Hamming distance and metric.
Wrenna Robson said:
What you want to do is define Codeword as Hamming (Fin n -> alpha)
i tried defining CodeWord the way that was suggested, but it doesn't seem to work? i don't quite get the type of Hamming
either, it seems to say it needs some kind of dependent type?
this is what i tried:
import Mathlib.Data.Fintype.Basic
import Mathlib.InformationTheory.Hamming
abbrev CodeWord (ι:Type) [Fintype ι] (Ω:Type) [DecidableEq Ω] : Type := Hamming (ι → Ω)
and this is the error i got:
application type mismatch
Hamming (ι → Ω)
argument
ι → Ω
has type
Type : Type 1
but is expected to have type
?m.1224 ι Ω → Type : Type 1
Wrenna Robson (Feb 09 2024 at 23:05):
Hmm, I can't quite remember how it's defined
Wrenna Robson (Feb 09 2024 at 23:06):
Wrenna Robson (Feb 09 2024 at 23:08):
Right yes I see - you're putting in the type \iota -> \omega. But actually you want something like this: const \iota \omega
Wrenna Robson (Feb 09 2024 at 23:09):
The other day after chatting about this I was playing around with definitions of the various delone quantities. I think I'm intending to redefine infsep to be the packing diameter at some point, and also define covering radius
Edward van de Meent (Feb 09 2024 at 23:11):
this seemed to work: @Hamming ι (fun x => Ω)
Wrenna Robson (Feb 09 2024 at 23:11):
Yes that's essentially the same
Edward van de Meent (Feb 09 2024 at 23:11):
sadly const doesn't seem to be a built-in
Wrenna Robson (Feb 09 2024 at 23:11):
Function.const maybe?
Wrenna Robson (Feb 09 2024 at 23:12):
Sorry I just got back from a week of house hunting, I'm pretty pooped ;_;
Edward van de Meent (Feb 09 2024 at 23:14):
Wrenna Robson said:
Function.const maybe?
you're right, that does work! and that way i don't need to specify the implicit context parameter too! thanks!
Wrenna Robson (Feb 09 2024 at 23:17):
Nw
Wrenna Robson (Feb 09 2024 at 23:18):
One thing I got stuck on was that not all codes use the hamming metric
Wrenna Robson (Feb 09 2024 at 23:18):
But I'm interested to see where you get to
Edward van de Meent (Feb 09 2024 at 23:22):
the plan is to define linear codes afterward, along with isomorphisms of linear codes...
speaking of, is there some reason why those are defined to conserve distance on the entire vectorspace, rather than just on the code? i couldn't figure it out, and there didn't seem to be some obvious proof that those are the same...
Wrenna Robson (Feb 09 2024 at 23:30):
How do you mean?
Wrenna Robson (Feb 09 2024 at 23:31):
Which distance?
Wrenna Robson (Feb 09 2024 at 23:31):
Anyway, an isometry of the space preserves distances.
Wrenna Robson (Feb 09 2024 at 23:31):
It would be strange to define an isometry only on a set...
Wrenna Robson (Feb 09 2024 at 23:32):
But of course you could define some notion of isometryOn...
Edward van de Meent (Feb 09 2024 at 23:40):
i see my mistake now... a key aspect of a Code is its embedding in the space of all possible codewords, since that's the space from where you want to be able to correct. i thought that it (for a linear code at least) was just some set with a notion of adding, scalar multiplying, and a notion of hamming distance on that set.
Wrenna Robson (Feb 09 2024 at 23:40):
Indeed, but it is not - the embedding is important
Wrenna Robson (Feb 09 2024 at 23:41):
It's a subset, or subspace in the case of a linear code
Wrenna Robson (Feb 09 2024 at 23:41):
But as I say not all codes use the hamming distance
Wrenna Robson (Feb 09 2024 at 23:41):
Wrenna Robson (Feb 09 2024 at 23:41):
Indeed it's not even necessary in theory that they be finite
Wrenna Robson (Feb 09 2024 at 23:42):
At least the underlying space - I think in practice you would always want a code to be finite, and of course in any practical application infinity doesn't exist
Edward van de Meent (Feb 09 2024 at 23:44):
right... i'm not sure how i would have to extend the definition that i have now though... something i (or someone else) will have to figure out later
Wrenna Robson (Feb 09 2024 at 23:44):
Broadly speaking, a "code" can be thought of as just some set in an arbitrary type, such that the set is sufficiently separated that I can distinguish members of the code, and so that sufficiently large balls around the codewords cover the set
Wrenna Robson (Feb 09 2024 at 23:45):
That is, really, a delone set. Many theorems about "codes" are actually theorems in that much more general setting
Wrenna Robson (Feb 09 2024 at 23:45):
But yes - what you should do is continue your work and hopefully someone will generalise it later
Wrenna Robson (Feb 09 2024 at 23:45):
Wrenna Robson (Feb 09 2024 at 23:46):
Proving the hamming bound would be a good test
Wrenna Robson (Feb 09 2024 at 23:46):
And then proving facts about perfect codes is the natural next step
Wrenna Robson (Feb 09 2024 at 23:47):
If you could prove this result it would be a very fine thing indeed: https://epubs.siam.org/doi/abs/10.1137/0124010?journalCode=smjmap
Edward van de Meent (Feb 09 2024 at 23:51):
i'm afraid i might fall short of those last two... the main reason i'm developing this part of the library is because i'd like a rigorous notion of code automorphisms, as the construction of the sporadic Mathieu-12 group depends in part on it (, or at least in the book i'm reading it does). i might give it a shot though
Wrenna Robson (Feb 09 2024 at 23:53):
Oh exciting
Wrenna Robson (Feb 09 2024 at 23:54):
The reason I suggest it is just that testing your definitions actually work for proving things is a great way to see if they're any good
Edward van de Meent (Feb 10 2024 at 15:39):
i'm having a bit of trouble... the packing distance in a metric space is half the smallest distance between points... however, for codes with the hamming distance, the packing distance is rounded down... is there a good way to unify this? if there isn't, which definition should i use?
there might be several options:
- the largest radius such that all open balls around points in the subset are disjoint
- this one would suggest rounding up
- the largest radius such that there is a all closed balls around points in the subset are disjoint, and there is some point where the shortest distance to a point in the subset is that radius
- this one agrees with the definition saying to round down.
- however, it only works in the discrete case, in the continuous case the limsup might give a value for which the property doesn't hold
- keep it as-is, half the smallest distance
Edward van de Meent (Feb 10 2024 at 15:42):
i feel the key to this problem is that in the discrete case, looking at a closed set makes more sense. in particular because it is sensible to only consider packing distances where there actually is some point with that distance to the subset
Edward van de Meent (Feb 10 2024 at 15:44):
somehow you'd want to look at both open and closed balls, and look at which combination of open/closed and radius fits the maximum amount of points in balls, while keeping the property that the balls around points in the subset are disjoint
Edward van de Meent (Feb 10 2024 at 15:45):
is there some mathematical concept that describes this?
Johan Commelin (Feb 10 2024 at 15:45):
It might help to write down a bunch of such statements in Lean, and prove them with sorry
. And then at some point the API might suggest what the optimal definition is.
Johan Commelin (Feb 10 2024 at 15:46):
Or you make all 3 definitions, and some implications between them...
Edward van de Meent (Feb 10 2024 at 15:48):
i was kindof thinking of somehow generalising this notion of "picking the largest radius that exists, such that all closed or all open balls are disjoint"
Edward van de Meent (Feb 10 2024 at 15:48):
but that will make properties a bit harder, because you don't necessarily know if you are talking about opens or closeds
Wrenna Robson (Feb 10 2024 at 15:49):
Yeah I know the issue you're talking about
Wrenna Robson (Feb 10 2024 at 15:50):
The easiest way to think about it I think is: the hamming metric is integer-valued, so "half" rounds down
Edward van de Meent (Feb 10 2024 at 15:51):
yes... except that when you use s.infsep
, it becomes real-valued automatically
Wrenna Robson (Feb 10 2024 at 15:52):
Yes, it's because we have no notion really of an integer-valued distance
Wrenna Robson (Feb 10 2024 at 15:52):
but
Wrenna Robson (Feb 10 2024 at 15:54):
https://en.m.wikipedia.org/wiki/Delone_set
Wrenna Robson (Feb 10 2024 at 15:54):
I think you want to use the definition here
Wrenna Robson (Feb 10 2024 at 15:54):
Like it's still true that open balls of radius infsep/2 won't intersect
Wrenna Robson (Feb 10 2024 at 15:55):
But - ah yeah right sorry, this is why one rounds up I think...
Wrenna Robson (Feb 10 2024 at 16:01):
If it's t-error correcting, then closed balls of radius t won't intersect. So in other words, the infsep has to be at least 2t + 1, right? If it was 2t, then there would be some pair with 2t coordinates different, but then if you change t of one to the coordinates of the other, that's t away from two codewords, and we can't correct it
Wrenna Robson (Feb 10 2024 at 16:06):
I think infsep/2 is the only sensible definition of packing radius. But it might mean that some of the literature doesn't quite line up. What I found was that defining it in terms of the balls isn't the way to go - you kinda want to treat that as a property you prove
Wrenna Robson (Feb 10 2024 at 16:07):
Especially because you can then say "ah well if e > packing radius, balls of that radius intersect", and that's true for I think both open and closed balls
Wrenna Robson (Feb 10 2024 at 16:08):
I recently tried writing some of this down - if you search on Zulip I think I posted some of it?
Edward van de Meent (Feb 10 2024 at 16:08):
Wrenna Robson said:
Especially because you can then say "ah well if e > packing radius, balls of that radius intersect", and that's true for I think both open and closed balls
this is not the case though?
Wrenna Robson (Feb 10 2024 at 16:09):
Is it not? I suppose it might not be
Edward van de Meent (Feb 10 2024 at 16:09):
if you take the entire space as your code, infsep will be 1. so then the packing radius is 1/2, but open balls of size 3/4 don't intersect
Edward van de Meent (Feb 10 2024 at 16:10):
even open balls of radius 1 don't
Wrenna Robson (Feb 10 2024 at 16:10):
Around each point in the space?
Edward van de Meent (Feb 10 2024 at 16:10):
yes
Edward van de Meent (Feb 10 2024 at 16:10):
in the discrete case
Wrenna Robson (Feb 10 2024 at 16:10):
Yeah.
Wrenna Robson (Feb 10 2024 at 16:11):
Oh yes of course because there's no "points in-between"
Wrenna Robson (Feb 10 2024 at 16:11):
Which is why my geometric intuition is messing up
Wrenna Robson (Feb 10 2024 at 16:13):
Whereas in lattice theory obviously they embed in a larger space... hmm
Wrenna Robson (Feb 10 2024 at 16:15):
What I suppose is true is that closed balls with radius infsep around a point in the space will always contain another point in the space
Wrenna Robson (Feb 10 2024 at 16:15):
I think that's true in the continuous and discrete cases?
Edward van de Meent (Feb 10 2024 at 16:15):
yes, by definition of infsep
Edward van de Meent (Feb 10 2024 at 16:16):
it gives you the pair of points in the subset of that distance
Wrenna Robson (Feb 10 2024 at 16:17):
The abstract of this paper looks interesting and promising
Wrenna Robson (Feb 10 2024 at 16:17):
https://link.springer.com/article/10.1007/s10623-012-9623-4
Wrenna Robson (Feb 10 2024 at 16:22):
Yeah here is a neat but troubling example
Wrenna Robson (Feb 10 2024 at 16:22):
f867cdc2-dbbf-4e4e-a6cb-02cc3cf9f5e1.jpg
Wrenna Robson (Feb 10 2024 at 16:24):
(note this is using the language of permutation codes)
Wrenna Robson (Feb 10 2024 at 16:24):
But the idea is - you can construct two codes, both with min distance 6, but one of them can decode 3 errors and one can't.
Edward van de Meent (Feb 10 2024 at 16:25):
yea, i got that much
Wrenna Robson (Feb 10 2024 at 16:25):
If the min distance is 3, you can guarantee you can decode 2 errors, but you might not be able to decode 3
Wrenna Robson (Feb 10 2024 at 16:26):
It suggests that in fact you do want to define the packing radius distinctly to infsep - it's that the minimum distance of the code is closely related to the packing radius, but I think it might be the case that you can't actually determine one from the other
Wrenna Robson (Feb 10 2024 at 16:26):
Annoying!!
Wrenna Robson (Feb 10 2024 at 16:27):
Also, making this definition in a way that is nicely compatible with the continuous case will be a pain, and it's never fun to be taking minimums.
Edward van de Meent (Feb 10 2024 at 16:28):
i think in general i'd need to formalise these notions:
class GMetricSpace A Codomain
def packing_radius (...) : (OpenOrClosed \x Codomain)
with OpenOrClosed an enum.
Wrenna Robson (Feb 10 2024 at 16:29):
Maybe - there was certainly some talk of doing generalised metric spaces at some point
Wrenna Robson (Feb 10 2024 at 16:29):
Basically all this is why I gave up before - it felt like the kind of thing that was too big to do alone, because you end up with a bunch of different ways of doing a bunch of stuff, and you want some coordination
Edward van de Meent (Feb 10 2024 at 16:30):
in that case, you can determine the radius simply by taking the supremum of radii that work in the closed case, while the enum is determined afterwards by checking wether a counterexample to the edge case exists
Wrenna Robson (Feb 10 2024 at 16:31):
Yeah no I just mean that you end up wanting a lot of general API
Wrenna Robson (Feb 10 2024 at 16:31):
That approach sounds hacky but if it lets you move forward it's better than nothing
Edward van de Meent (Feb 10 2024 at 16:34):
the question is if i should keep calling such a space a DeloneSet
or not...
Wrenna Robson (Feb 10 2024 at 16:34):
Yeah. Possibly not!
Wrenna Robson (Feb 10 2024 at 16:35):
But it feels like a useful notion to have and tantalisingly close to what you actually want
Wrenna Robson (Feb 10 2024 at 16:36):
I think possibly, as @Yaël Dillies has observed at some point, part of the issue is that "packing radius" is kinda less useful than "packing diameter".
Edward van de Meent (Feb 10 2024 at 16:36):
what's packing diameter?
Edward van de Meent (Feb 10 2024 at 16:38):
twice the radius of the largest sphere that does not contain an element of the subset?
Wrenna Robson (Feb 10 2024 at 16:40):
Infsep, probably.
Wrenna Robson (Feb 10 2024 at 16:40):
It's sort of like, intuitively, we can expand out to that diameter without hitting another codeword
Wrenna Robson (Feb 10 2024 at 16:40):
Or rather I suppose, that's the first time when we might
Wrenna Robson (Feb 10 2024 at 16:40):
Or when another codeword is an infinitesimal distance away?
Wrenna Robson (Feb 10 2024 at 16:41):
It doesn't help we don't even have a notion of discrete metric...
Edward van de Meent (Feb 10 2024 at 16:41):
right... let me get a start with general metrics, see how that goes
Edward van de Meent (Feb 10 2024 at 16:44):
i'm guessing the best general case for a notion of distance is a linear ordering with a lowest element?
Edward van de Meent (Feb 10 2024 at 16:46):
where we'd like the distance between an element and itself to be that lowest element?
Wrenna Robson (Feb 10 2024 at 16:49):
Uh. Well, you don't need the second part. I guess that would be a generalised pseudometric?
Edward van de Meent (Feb 10 2024 at 16:49):
so just any linear ordering?
Wrenna Robson (Feb 10 2024 at 16:56):
Well, for the dist function it can be anything, in a sense that's just notation.
Edward van de Meent (Feb 10 2024 at 16:57):
ah, there is a slight hiccup as we would like to be able to add distances to define the triangle inequality
Notification Bot (Feb 10 2024 at 16:57):
A message was moved here from #new members > How to get the least element of a set of natural numbers? by Edward van de Meent.
Edward van de Meent (Feb 10 2024 at 16:59):
i'm guessing we should like it to be a monoid which respects ordering? as in, adding only increases its value?
Yaël Dillies (Feb 10 2024 at 17:17):
Wrenna Robson said:
I think possibly, as Yaël Dillies has observed at some point, part of the issue is that "packing radius" is kinda less useful than "packing diameter".
I'm not sure I said this exactly, but I do agree that you can't just take the packing radius to be half the packing diameter.
Yaël Dillies (Feb 10 2024 at 17:19):
I will also point out that, just as we have both docs#Int.floor and docs#Int.ceil, you will very likely need both the left and right adjoint to some map (which I think is ε ↦ ball x ε
, but I'm not sure)
Edward van de Meent (Feb 10 2024 at 17:50):
the first hurdle has been cleared: writing a definition for a general equivalent to a PseudoMetricSpace.
it turns out you can easily extend it. The construction of a Bornology (whatever that is) still works. However, i was unable to extend the mapping to a Uniform space
Wrenna Robson (Feb 10 2024 at 20:09):
Yaël Dillies said:
I will also point out that, just as we have both docs#Int.floor and docs#Int.ceil, you will very likely need both the left and right adjoint to some map (which I think is
ε ↦ ball x ε
, but I'm not sure)
Oh this is a nice observation.
Edward van de Meent (Feb 10 2024 at 20:12):
i think that's precisely what will happen when i add the option between open or closed... not exactly sure, but i think so
Edward van de Meent (Feb 10 2024 at 21:35):
right now, i've defined the generalised metric to have domain β
with [LinearOrderedAddCommMonoid β]
, however in copying some lemmas of PseudoMetricSpace i often come across instances where i'd like to prove something like (a < b) -> (a + c < b + c)
, and the original proofs make use of some lemmas (in docs#Mathlib.Algebra.Order.Monoid.Lemmas) which require an instance [CovariantClass β β (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x < x_1]
... i'm not exactly sure how i should fix something like this, other than explicitly adding the instance and continuing... is there some single stronger requirement i could ask of β
? the trouble of expanding to something like [Group β] is that you'd probably have to allow negative distances...
Yaël Dillies (Feb 10 2024 at 23:19):
Look up docs#LinearOrderedAddCommMonoid
Yaël Dillies (Feb 10 2024 at 23:21):
See that it is extended by docs#LinearOrderedCancelAddCommMonoid
Edward van de Meent (Feb 11 2024 at 08:22):
Thanks!
Edward van de Meent (Feb 12 2024 at 19:58):
i'd like some advice...
right now i've defined a notion of generalised DeloneSet, and have a definition for a "general" Linear Code, i.e. a subspace of some vectorspace that is also a DeloneSet... however, now i'm not sure if there really is a difference between a DeloneSet and a code. furthermore, i'm not certain if i should add more requirements to Linear Codes, as the current notion really seems like the best definition that does not necessarily use the Hamming distance. i could of course add a requirement that the vectorspace must be a finite disjoint union of a finite field (or something like that), but that seems unnecessarily restrictive... what is the best course going forward?
Wrenna Robson (Feb 12 2024 at 19:59):
I'm not sure if there's a meaningful rather than contextual difference.
Wrenna Robson (Feb 12 2024 at 20:00):
Honestly what I would do is try to free yourself from definition hell by picking some simple theorems and trying to prove them.
Wrenna Robson (Feb 12 2024 at 20:00):
In my experience that is the best guide.
Wrenna Robson (Feb 12 2024 at 20:02):
Trying to remember what we call a module equipped with a compatible norm... There's a word for this. Anyway, all subspaces of the suitable vector space are linear codes - so it must be a property of the space, not the individual code
Wrenna Robson (Feb 12 2024 at 20:02):
Like there's something about the space that means all subspaces are delone, right?
Wrenna Robson (Feb 12 2024 at 20:03):
And that's weird. It's certainly not true of all subsets! But I wonder if it is the essential thing you need to capture
Edward van de Meent (Feb 12 2024 at 20:10):
Wrenna Robson said:
I'm not sure if there's a meaningful rather than contextual difference.
the differences that i can think of of the top of my head are twofold: the first difference is that right now, the vectorspace can have any number of dimensions (even infinite). secondly, as of yet there is no restriction on the "size" of the scalar field, so each of the dimensions can stretch on forever in every direction you'd like, which most certainly isn't the case for products of finite fields.
Wrenna Robson (Feb 12 2024 at 20:11):
But is this actually important for anything in the actual definition?
Wrenna Robson (Feb 12 2024 at 20:11):
Rather than an extra hypothesis you will introduce in certain theorems?
Edward van de Meent (Feb 12 2024 at 20:12):
well... if i want to at least be somewhat consistent with existing literature....
Wrenna Robson (Feb 12 2024 at 20:12):
I agree that there's a few finiteness constraints that you need for coding theory
Wrenna Robson (Feb 12 2024 at 20:13):
Edward van de Meent said:
well... if i want to at least be somewhat consistent with existing literature....
In my experience - I don't think I'm entirely wrong about this - the definitions in existing literature don't always match up with the natural way to formalise things, and it's very easy to unnecessarily introduce constraints into your definitions that aren't actually necessary for them.
Wrenna Robson (Feb 12 2024 at 20:14):
I personally take a formalisation philosophy that things should minimally use preconditions, only when they are necessary.
Wrenna Robson (Feb 12 2024 at 20:14):
Like in the literature sometimes a code is defined as a map and sometimes it's defined as the image of that map
Wrenna Robson (Feb 12 2024 at 20:14):
You literally can't be fully consistent.
Edward van de Meent (Feb 12 2024 at 20:15):
it can be a map :melting_face:
Edward van de Meent (Feb 12 2024 at 20:15):
welp
Wrenna Robson (Feb 12 2024 at 20:15):
And in my experience if you make your definitions too specialised, it becomes challenging to go on and use your definitions
Wrenna Robson (Feb 12 2024 at 20:15):
Well yeah of course
Wrenna Robson (Feb 12 2024 at 20:16):
Like another way of thinking about a linear code is that it's an injective linear map, right?
Wrenna Robson (Feb 12 2024 at 20:16):
Say from a space with dimension n to a space with dimension k
Wrenna Robson (Feb 12 2024 at 20:16):
And maybe we have a metric on the spaces which is, essentially, the hamming metric according to a particular basis for both of them
Wrenna Robson (Feb 12 2024 at 20:17):
Then the image of the map is the set of codewords.
Edward van de Meent (Feb 12 2024 at 20:17):
i hadn't thought about it that way, i had only come across the "it's a subset with those distance properties" part...
Wrenna Robson (Feb 12 2024 at 20:17):
OR it could be a surjective linear map from a space with dimension n to a space with dimension n - k, and the kernel is the set of codewords
Wrenna Robson (Feb 12 2024 at 20:18):
Because linear codes (well, any subspace, but in this context) are simultaneously images or kernels, and when they're images we think of them as codewords, and when they're kernels we think of them as sets with null syndromes
Edward van de Meent (Feb 12 2024 at 20:19):
the thing is, i think the requirements you pose on automorphisms make a lot more sense when you look at a Code (not necessarily a linear one) as a map, rather than a subset, as it makes it obvious that the "superspace" is important
Wrenna Robson (Feb 12 2024 at 20:19):
Yes. But the trouble is the choice of map is not unique
Wrenna Robson (Feb 12 2024 at 20:20):
Different encodings can give rise to the same codewords
Wrenna Robson (Feb 12 2024 at 20:20):
Which is why one makes the equation of the linear codes with the subspaces/subsets
Wrenna Robson (Feb 12 2024 at 20:20):
The trouble being that it does somewhat obscure these other properties/perspectives
Wrenna Robson (Feb 12 2024 at 20:21):
And the issue is that in formalisation, we really have to care about what things actually are, rather than making these kind of elisions where we equate stuff
Edward van de Meent (Feb 12 2024 at 20:22):
the main problem that i'm understanding from this is that given some distance function and set of codewords on some space, the mapping is not unique?
Wrenna Robson (Feb 12 2024 at 20:22):
Yes
Wrenna Robson (Feb 12 2024 at 20:22):
Another way of thinking about this is - you have many different generating sets for the same code
Wrenna Robson (Feb 12 2024 at 20:23):
Or sometimes you want to take one code and permute it to obscure its structure (this is relevant in cryptography).
Edward van de Meent (Feb 12 2024 at 20:26):
i don't think that different generating sets should be a problem the way i've linear codes right now... and i think permuting a code can be done by simply applying the permutation before both parameters of the metric and before the correcting map? that should still work, right?
Wrenna Robson (Feb 12 2024 at 20:34):
Correcting map?
Edward van de Meent (Feb 12 2024 at 20:34):
the mapping from the entire space to the codewords?
Wrenna Robson (Feb 12 2024 at 20:35):
Why is it called that?
Edward van de Meent (Feb 12 2024 at 20:37):
that's how i describe it. i'm not very familiar with coding theory, but that's what i'd call it. if it's not obvious or if there is a better/more common name for such a map, i do apologise, i didn't know.
Edward van de Meent (Feb 12 2024 at 20:37):
because the map corrects
Wrenna Robson (Feb 12 2024 at 20:38):
Oh I see, as in, the map that - right
Wrenna Robson (Feb 12 2024 at 20:38):
But you don't explicitly have such a map, right?
Wrenna Robson (Feb 12 2024 at 20:39):
I would call this operation "decoding", incidentally
Edward van de Meent (Feb 12 2024 at 20:39):
ah right, i remember seeing that somewhere...
Edward van de Meent (Feb 12 2024 at 20:42):
Wrenna Robson said:
But you don't explicitly have such a map, right?
no, i don't... but i'm thinking about it...
Edward van de Meent (Feb 12 2024 at 20:42):
i should at the very least consider it, before discarding such an idea
Wrenna Robson (Feb 12 2024 at 20:45):
You can certainly define such a map
Wrenna Robson (Feb 12 2024 at 20:45):
But you won't have a general explicit definition I think
Wrenna Robson (Feb 12 2024 at 20:46):
Not a computable one anyway
Edward van de Meent (Feb 12 2024 at 20:47):
yes, and extensionality would also be a weaker tool, precisely because there might be multiple decoding maps
Wrenna Robson (Feb 12 2024 at 20:49):
Well ideally it is unambiguous what they decode to, so from a function extensionality pov they're all the same, but I think one can certainly say of a function "this function decodes that code"
Edward van de Meent (Feb 12 2024 at 20:52):
yes, i can certainly write such a statement... something along the lines of "the function maps all closed balls of a certain radius around some codepont to that codepoint if they don't intersect with some other ball with that radius around another codepoint"
Wrenna Robson (Feb 12 2024 at 20:54):
Yeah the issue I guess is that you do have a limit to how much you can correct
Wrenna Robson (Feb 12 2024 at 20:54):
And Ithink that when it's not a perfect code, there will be things that cannot be corrected to anything
Edward van de Meent (Feb 12 2024 at 20:55):
yes, that does seem right
Edward van de Meent (Feb 12 2024 at 21:04):
i suppose you could construct a decoding map in general by doing axiom of choice on the family of sets of closest codewords for each point... but it wouldn't exactly be canonical
Edward van de Meent (Feb 12 2024 at 21:06):
by the way, is there a name for the union of those closed balls i was talking about? or can i give it a name like "sphere of influence" or something?
Wrenna Robson (Feb 12 2024 at 21:22):
Crucially I think decoding is NP hard in general
Wrenna Robson (Feb 12 2024 at 21:23):
Hmm not sure. Name it and it can be renamed later.
Edward van de Meent (Feb 12 2024 at 21:27):
def Separates (c:GDeloneSet α₁ β) (δ : β): Prop :=
∀ cw ∈ c, ∀ cw' ∈ c, cw ≠ cw' → closedBall cw δ ∩ closedBall cw' δ = ∅
def IsDecodingMap (c : GDeloneSet α₁ β) (DecFun : α₁ → c):Prop :=
∀ x : α₁, ∀ cw ∈ c, Separates β c (GDist.gdist x cw) → DecFun x = cw
sneak peek
Edward van de Meent (Feb 12 2024 at 21:28):
here beta is the type of the codomain of the metric we're using. it gets passed because lean doesn't always naturally infer the type we're going for
Edward van de Meent (Feb 16 2024 at 20:11):
i'm having some trouble with defining the covering radius... according to the source that was mentioned before, it is the smallest distance such that closed balls around elements of some set X
cover the entire space, however it seems to me that when you choose X={1/n | n∈ℕ}
and the entire space X∪ {-1}
, the infimum of distances which cover {-1}
is equal to 1, however closed balls around elements of X
with radius 1 all don't contain the element {-1}
... so there is no such smallest distance...
is this just a bad description or definition of covering radius? or is there some assumption i'm missing?
Wrenna Robson (Feb 16 2024 at 20:12):
Just so you know, @Newell Jensen is also interested in some of these things and is pursuing a patch to add some of these concepts
Wrenna Robson (Feb 16 2024 at 20:13):
Yeah I think it is the infimum of something, but it may not imply that it does cover the space
Wrenna Robson (Feb 16 2024 at 20:13):
You might need an extra assumption on the space (completeness?)
Edward van de Meent (Feb 16 2024 at 20:16):
i think that would fix it yea.... or maybe something like the subset of elements closer than some radius is finite, maybe?
Edward van de Meent (Feb 16 2024 at 20:17):
i'm not completely sure
Wrenna Robson (Feb 16 2024 at 20:17):
Perhaps.
Newell Jensen (Feb 16 2024 at 20:18):
@Edward van de Meent feel free to contribute to #10641 if you see fit.
Edward van de Meent (Feb 16 2024 at 20:21):
thanks... although i did use my own definitions and stuff, so it might not exactly be compatible... in particular i generalised it so discrete metrics and anything inbetween could be used...
Edward van de Meent (Feb 16 2024 at 20:22):
most of my definitions parametrise over some codomain β
which is a CompleteLinearOrder
and a AddCommMonoid
, along with a mixin which says that they work together nice...
Edward van de Meent (Feb 16 2024 at 20:24):
that way, some distances come out a bit better
Wrenna Robson (Feb 16 2024 at 20:24):
It might be good to state some goals: I think broadly what we are looking for here is, aside from the specific context of coding theory, to get concepts such as Delone sets, packing radii, minimum distance and so forth to a) lie flat together, b) be defined in Mathlib to an appropriate degree of generality i.e. for as arbitrary a metric space as possible.
Wrenna Robson (Feb 16 2024 at 20:25):
The wrinkles come in because in the literature, different definitions are sometimes used, and in general settings they might not be equivalent.
Wrenna Robson (Feb 16 2024 at 20:25):
Does that reflect both your understandings?
Wrenna Robson (Feb 16 2024 at 20:25):
Actually I should post this in the other thread...
Nurrin (Nov 26 2024 at 12:50):
Hi everyone,
I am currently interested in starting a project in sphere-packing bound. I'd like to ask what is the current status of Information Theory in Mathlib. Are there any existing ongoing projects related to this area that I should be aware of before starting ? So far as I know, there is already a formalisation of the Hamming distance, but I'm unsure about the overall state of the field in Mathlib.
I'd greatly appreciate any feedback. Thank you in advance for your time and insights.
Best regards,
Nurrin
Sidharth Hariharan (Nov 26 2024 at 13:08):
Hi Nurrin,
I am currently working with several others on a project to formalise the solution to the sphere packing problem in dimension 8. We have built a nontrivial amount of machinery, including definitions and lemmas on things like sphere packing density, which might be of interest to you. You can read the blueprint and look at our documentation, but the repo itself is still private. Is this the sort of thing you had in mind? (I know close to nothing about information theory.)
Nurrin (Nov 26 2024 at 15:11):
Hi Sidharth,
Thank you for letting me know. I would want to work on the sphere-packing bound in coding theory, using the Hamming metric. I believe it is quite a different topic.
Junyan Xu (Nov 26 2024 at 22:01):
There are definitely connections, e.g. between the binary Golay code and the Leech lattice. This chapter of SPLAG has more details.
Junyan Xu (Nov 26 2024 at 22:10):
Glad to learn that the E8 project is now in progress! I think @Seewoo Lee would also be pleased to be informed. People have been discussing multivariate Poisson summation here because I made a comment about the linear programming bound (Theorem 4.7/5.1 in the blueprint). Is LinearProgrammingBound already sorry free? (Update: I found the answer here: looks like its derivation from the Poisson summation formula is formalized but the Possion formula is not.)
By the way, I believe the sphere-packing bound in coding theory is this one: https://en.wikipedia.org/wiki/Hamming_bound#Statement_of_the_bound
Seewoo Lee (Nov 26 2024 at 23:10):
@Junyan Xu Yes I'm actually in the Sidharth's group too :) But as Nurrin said, it seems that the one for coding theory and Viazovska's result are different things.
Sidharth Hariharan (Nov 27 2024 at 23:09):
Nurrin said:
Hi Sidharth,
Thank you for letting me know. I would want to work on the sphere-packing bound in coding theory, using the Hamming metric. I believe it is quite a different topic.
I see, never mind then :)
I don't know any information theory at all :D
That being said, thanks @Junyan Xu for sharing the link to the book. One of my friends was coincidentally just talking to me about something he did with Hamming metrics (not in Lean or anything), and it definitely does sound interesting. I'll def read about it if I get a chance.
Last updated: May 02 2025 at 03:31 UTC