IsaKim (Feb 25 2025 at 10:06): IsaKim (Feb 25 2025 at 10:06):Dear all, I am writing to ask for help in defining linear functional in terms of the definitions about vector spaces in HOL.Vector_Spaces (and using locale in general). I am trying to formally define a linear functional in a programmatic way, but I am encountering numerous errors. A linear functional $p$ is a function on a vector space that satisfies the following properties:
It takes a vector as input and outputs a real number.
$p(x+y)=p(x)+p(y)$ for any vectors $x$ and $y$.
$p(kx)=k⋅p(x)$. for any scalar $k$ and vector $x$.
Could someone please advise me on which files or resources I should study to correctly define a linear functional? Any guidance would be greatly appreciated.
error.png
I am currently working on formalizing the properties of the Dirac delta function, which is an element of the space of distributions. Since the space of distributions is the dual space of the space of test functions, it is essential to define a linear functional properly. This is because the Dirac delta function acts as a linear functional on the space of test functions. Could you kindly suggest which files or resources I should refer to for defining a linear functional correctly? This would be immensely helpful for my work on elucidating the properties of the Dirac delta function as a linear functional. Thank you very much for your assistance.
terru (Feb 25 2025 at 15:36):('a, 'b) vec comes with sort constraints, which aren't met here: it requires that 'a::times and 'b::finite (i.e. that 'a has an instance of the times class, and 'b of the finite class), which you'd need to add to your locale as sort constraints, e.g. by simply writing ::times behind the 'a in fixes to make sure the locale can satisfy these constraints.
but even with that your assumption as written would not type check, because in a * p x you're trying to multiply a real with an 'a, which can't work. Maybe you can either change the type of p to (real, 'b::finite) vec ⇒ real or to ('a::times, 'b::finite) vec ⇒ 'a, depending on whether you want your theory to be about vector spaces based on real or something more general? (if the latter, you will also need that 'a has an instance of plus, so write 'a :: {times, plus}). You might also want to read more about type classes and locales in the locales/classes tutorials (in the documentation panel)
Yong Kiam (Feb 26 2025 at 01:10):hi, I am not sure if this will help, but you may want to have a look at:
https://www.isa-afp.org/sessions/ordinary_differential_equations/#Bounded_Linear_Operator.html
or more specifically at Bounded_Linear_Function in HOL-Analysis
Chelsea Edmonds (Feb 26 2025 at 16:22):It might interest you that there is another vector space library in the AFP which is pretty widely used (https://www.isa-afp.org/entries/VectorSpace.html). I believe it is slightly more general, also done using locales. I used this (and the follow on libraries on vectors/matrices provided in the Jordan Normal Form entry) for past work in linear algebra personally.
Chelsea Edmonds (Feb 26 2025 at 16:28):Re using locales generally, beyond the tutorial, Larry has written a really good blog article introducing the general approach used on several of the ALEXANDRIA project formalisations with locales: https://lawrencecpaulson.github.io/2022/03/23/Locales.html. Several of my papers give other examples, and happy to recommend more resources/other good papers if you'd like!
Last updated: Feb 28 2025 at 08:24 UTC