Email Gateway (Aug 22 2022 at 12:43): Email Gateway (Aug 22 2022 at 12:43):From: Esseger <esseger@free.fr>
Hello,
I am looking for a good way to express some basic mathematical objects
in the current Isabelle/HOL framework.
Here is a representative example of my question. Let 'a be a compact
metric space. Then a function f from 'a to real numbers is c-Hölder
continuous (where c>0 is some given positive real number) if it is
continuous and
(*_c) : sup_{x \neq y} |f(x)-f(y)|/ d(x,y)^c
is finite. It is easy to check that the set of c-Hölder continuous
functions is a Banach space, for the norm equal to the sup norm plus *_c.
In a mathematical paper, I would write this as:
Thm: Let X be a compact metric space, let c>0. Then the set of c-Hölder
continuous functions on X (with the above norm) is a Banach space.
My question is how to express this theorem in Isabelle/HOL in the best
way using locales/type classes (given that Banach spaces are type
classes). And then write conveniently statements such as: the inclusion
of c-Hölder continuous functions in d-Hölder continuous functions is a
continuous injection when d<c.
Any hint?
Best,
Esseger
Email Gateway (Aug 22 2022 at 12:56):From: Esseger <esseger@free.fr>
Maybe I wasn't clear enough that the only problem I have is that the
Banach spaces depend on a parameter. A similar question would arise when
defining for instance the L^p spaces, for p in [1, \infty) (maybe the
most prominent missing block in Multivariate_Analysis).
Does the absence of answer mean that there is no nice way to do this in
current Isabelle, and that tools with dependent type theory such as CoQ
would be better suited for the task? That would be very sad in my
opinion, as Isar is by far more mathematician-friendly, and the analysis
libraries are also by far superior in Isabelle/HOL.
Best,
Esseger
Email Gateway (Aug 22 2022 at 12:57):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Esseger,
one option you would have is to somehow encode the parameter in a type.
For example you could use Numeral_Types to represent natural numbers at
the type level, as it is done in Multivariate_Analysis.
Another hack is to introduce a type class real_value:
class real_value =
fixes real_value :: 'a itself => real
which assign to an arbitrary type a real value. Then you could express
c-Hölder continuous functions as a type. And also your inclusion
statement:
lemma
fixes C :: "'c :: real_value" and D :: "'c :: real_value"
assumes "real_value ITSELF('c) > real_value ITSELF('d)"
shows "EX i :: ('a, 'c) hölder => ('a, 'd) hölder. ..."
...
Problem is: it is currently not possible to construct a
"'a::real_value" in a proof! Ondřej Kunčar and Andrei Popescu work on a
solution but it is not there yet.
I hope this helps!
- Johannes
Email Gateway (Aug 22 2022 at 12:58):From: Esseger <esseger@free.fr>
Thanks a lot for your answer, indeed it helps! Although as far as I
understand I have the impression that some useful constructions would
not be expressible in this formalism. For instance, would it be possible
in this way to define the integrability exponent of a function, i.e.,
Sup {p. f \in L^p} ?
Or do an induction on (integer) integrability exponents?
Esseger
Email Gateway (Aug 22 2022 at 13:01):From: Johannes Hölzl <hoelzl@in.tum.de>
Hm, I think defining the integrability exponent of a function is not
possible in a nice way. But in this specific case you can unfold the
definition itself:
Sup {p. |f^p| has_integral}
I'm not sure about induction on (integer) integrability exponents...
Last updated: Apr 24 2024 at 01:07 UTC