analysis icon indicating copy to clipboard operation
analysis copied to clipboard

Published 20 hours ago • verified publisher icon math-comp

Lspace

Open hoheinzollern opened this issue 1 year ago • 2 comments

This PR will be rebased on PR #1506 (or on master should the latter be merged before).

hoheinzollern avatar May 27 '24 08:05 hoheinzollern

The CI error is:

       > COQC theories/lspace.v
       > File "./theories/lspace.v", line 82, characters 33-42:
       > Error: Syntax error: [reduce] expected after ':=' (in [def_body]).

affeldt-aist avatar May 28 '24 13:05 affeldt-aist

Wikipedia uses the p-norm to define Lp spaces when p may be +oo, whereas for example this reference sticks to the definition that was previously in this PR. Klenke also seems to go with the Wikipedia approach. I have now moved to using norms in the last commits, and extending the theory to extended reals. Is there a good reason to choose one over the other?

hoheinzollern avatar Aug 16 '24 08:08 hoheinzollern