Lspace #1230
Lspace #1230
Conversation
|
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]). |
|
Wikipedia uses the p-norm to define Lp spaces when |
- better interface in lspace.v
| match p with | ||
| | r%:E => [get q : R | r^-1 + q^-1 = 1]%:E | ||
| | +oo => 1 | ||
| | -oo => 0 | ||
| end. |
There was a problem hiding this comment.
This is ill-defined when p = 1, writing the following
| match p with | |
| | r%:E => [get q : R | r^-1 + q^-1 = 1]%:E | |
| | +oo => 1 | |
| | -oo => 0 | |
| end. | |
| [get q : \bar R | (q > 0) /\ r^-1 + q^-1 = 1] |
with a proper definition of ^-1 that I might PR soon.
theories/lspace.v
Outdated
| Lemma ess_sup_cst_lty r : (0 < mu setT)%E -> (ess_sup mu (cst r) < +oo)%E. | ||
| Proof. | ||
| rewrite /ess_sup => mu0. | ||
| under eq_set do rewrite preimage_cst/=. | ||
| rewrite ereal_inf_EFin ?ltry//. | ||
| - exists r => x/=; case: ifPn => [_|]. | ||
| by move: mu0 => /[swap] ->; rewrite ltNge lexx. | ||
| by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE. | ||
| by exists r => /=; rewrite ifF//; rewrite set_itvE; | ||
| rewrite memNset //=; apply/negP; rewrite -real_leNgt ?num_real. | ||
| Qed. | ||
|
|
||
| Lemma ess_sup_cst r : (0 < mu setT)%E -> (ess_sup mu (cst r) = r%:E)%E. |
There was a problem hiding this comment.
The former lemma is subsumed by the latter.
There was a problem hiding this comment.
no need to have it indeed
theories/lspace.v
Outdated
| Qed. | ||
|
|
||
|
|
||
| Lemma Lnorm_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. |
There was a problem hiding this comment.
Add a lemma saying forall f : ty, nm f = 'N[mu]_p[f]%:E
| Require Import -(notations) Setoid. | ||
|
|
||
| Declare Scope signature_scope. | ||
| Delimit Scope signature_scope with signature. | ||
| Import -(notations) Morphisms. | ||
| Module ProperNotations. | ||
|
|
||
| Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) | ||
| (right associativity, at level 55) : signature_scope. | ||
|
|
||
| Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature)) | ||
| (right associativity, at level 55) : signature_scope. | ||
|
|
||
| Notation " R ~~> R' " := (@respectful _ _ (Program.Basics.flip (R%signature)) (R'%signature)) | ||
| (right associativity, at level 55) : signature_scope. | ||
|
|
||
| End ProperNotations. | ||
| Import ProperNotations. | ||
|
|
||
| Arguments Proper {A}%_type R%_signature m. | ||
| Arguments respectful {A B}%_type (R R')%_signature _ _. |
There was a problem hiding this comment.
This should be in a dedicated compat file for importing setoid rewrite into MCA.
| Lemma ess_supP f a : | ||
| ess_sup f = a <-> \forall x \ae mu, (f x)%:E <= a. |
There was a problem hiding this comment.
| Lemma ess_supP f a : | |
| ess_sup f = a <-> \forall x \ae mu, (f x)%:E <= a. | |
| Lemma ess_supP f a : | |
| reflect (\forall x \ae mu, (f x)%:E <= a) (ess_sup f <= a). |
There was a problem hiding this comment.
@hoheinzollern I can try to contribute this lemma if you haven't done it somewhere else.
There was a problem hiding this comment.
This is the main theorem about essential supremums i.e. "ess_sup ⊣ (<=_ae)", and essentially everything comes from this
|
(deleted comment) |
|
I can see there was activity. Shall I close this PR? It looks no longer relevant. |
|
I closed it by mistake. I think that it should be rebased on top of master because iirc it was going a step further by using a feature of MathComp that was only available in master. |
3 participants
This PR will be rebased on PR #1506 (or on master should the latter be merged before).