# Re: [isabelle] Type classes and parameters

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...

- Johannes

Am Donnerstag, den 03.03.2016, 23:34 +0100 schrieb Esseger:
> 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
>
> Le 03/03/2016 10:05, Johannes HÃlzl a Ãcrit :
> > 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
> >
> >
> > Am Mittwoch, den 02.03.2016, 22:30 +0100 schrieb Esseger:
> > > 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
> > >
> > >
> > >
> >
> >
>
>
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.