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.