Stream: math-comp analysis

Topic: using near


view this post on Zulip Marie Kerjean (Nov 25 2020 at 20:31):

Is there a lemma statingforall e, 0< e -> x \is_near (nbhs 0)) -> |x| < e` in a normed vector space ?

view this post on Zulip Cyril Cohen (Nov 25 2020 at 22:44):

Marie Kerjean said:

Is there a lemma statingforall 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)

view this post on Zulip Cyril Cohen (Nov 25 2020 at 22:50):

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.

view this post on Zulip Marie Kerjean (Nov 26 2020 at 10:53):

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'?

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:01):

which tactic / line of tactics did you use to get the locked_with (you are now supposed to get there)

view this post on Zulip Marie Kerjean (Nov 26 2020 at 11:11):

I have a goal |e| <r on which I use the tactic near: e.

view this post on Zulip Marie Kerjean (Nov 27 2020 at 08:57):

Is the tactic correct ? Could the fact that locked_with is appearing be a consequence of a bad join/type structure on R[i] ?

view this post on Zulip Cyril Cohen (Nov 27 2020 at 08:59):

can you point me to a branch where this happens?

view this post on Zulip Marie Kerjean (Nov 27 2020 at 09:41):

here for example : https://github.com/math-comp/analysis/blob/04718df0d021fa96dba178c258e880f2e95c0e11/theories/holomorphy.v#L740.

view this post on Zulip Cyril Cohen (Nov 27 2020 at 12:01):

I will take a look

view this post on Zulip Cyril Cohen (Nov 27 2020 at 12:30):

So, here is the explanation:

view this post on Zulip Cyril Cohen (Nov 27 2020 at 12:31):

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.

view this post on Zulip Cyril Cohen (Nov 27 2020 at 12:31):

you could then do move: r r0; near: e, but I expect you will fail...

view this post on Zulip Cyril Cohen (Nov 27 2020 at 12:34):

I do not understand how this proof though ....

view this post on Zulip Marie Kerjean (Nov 27 2020 at 12:53):

So I shouldn' t use near: e on a goal containing free variables triggering constraints on e ?

view this post on Zulip Marie Kerjean (Nov 27 2020 at 12:54):

Cyril Cohen said:

I do not understand how this proof though ....

I'm not sure In understand your comment.

view this post on Zulip Cyril Cohen (Nov 27 2020 at 13:01):

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

view this post on Zulip Cyril Cohen (Nov 27 2020 at 13:02):

Marie Kerjean said:

So I shouldn' t use near: e on a goal containing free variables triggering constraints on e ?

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.

view this post on Zulip Marie Kerjean (Nov 27 2020 at 13:03):

of course, thanks !


Last updated: Aug 11 2022 at 01:03 UTC