Is there a lemma statingforall e, 0< e -> x \is_near (nbhs 0)) ->
|x| < e` in a normed vector space ?
Marie Kerjean said:
Is there a lemma stating
forall e, 0< e -> x \is_near (nbhs 0)) ->
|x| < e` in a normed vector space ?
No, I think it is missing, but it should definitely be added! (the proof should be a one-liner)
Lemma nbhs0_lt (R : numFieldType) (V : normedModType R) e :
0 < e -> \forall x \near (nbhs (0 : V)), `|x| < e.
Proof.
move=> e_gt0; apply/nbhs_ballP; exists e => // x.
by rewrite -ball_normE /= sub0r normrN.
Qed.
Another question on the use of near. After discharging
e : (R[i])^o
_Hyp_ : e \is_near (nbhs (nbhs' 0))
I get a locked goal :
locked_with near_key (forall x0 : (R[i])^o, x0 \is_near (nbhs (nbhs' 0)) -> `|x0| <r)
I cannot apply the previous lemmas and rewriting through rewrite locked_withE
gets me at strange places (where there are mismatches on @default_arrow_filter
types) . Any insight about what I should do ? Is that because of the use of nbhs'
?
which tactic / line of tactics did you use to get the locked_with
(you are now supposed to get there)
I have a goal |e| <r
on which I use the tactic near: e
.
Is the tactic correct ? Could the fact that locked_with
is appearing be a consequence of a bad join/type structure on R[i]
?
can you point me to a branch where this happens?
here for example : https://github.com/math-comp/analysis/blob/04718df0d021fa96dba178c258e880f2e95c0e11/theories/holomorphy.v#L740.
I will take a look
So, here is the explanation:
there seems to a bug in near:
, the call to near: e
should have failed with error message : impossible to infer r that does not depend on e, you might want to generalize r (as in move: r e) or introduce r before using near=> e
.
you could then do move: r r0; near: e
, but I expect you will fail...
I do not understand how this proof though ....
So I shouldn' t use near: e
on a goal containing free variables triggering constraints on e
?
Cyril Cohen said:
I do not understand how this proof though ....
I'm not sure In understand your comment.
Marie Kerjean said:
Cyril Cohen said:
I do not understand how this proof though ....
I'm not sure In understand your comment.
I do not understand ~how~ this proof ~works~ though ....
Marie Kerjean said:
So I shouldn' t use
near: e
on a goal containing free variables triggering constraints one
?
Sure, you cannot say a e
should be bigger/smaller than a quantity that depends on e
... that would be a circular dependency and it is forbidden.
of course, thanks !
Last updated: Oct 13 2024 at 01:02 UTC