Is there a lemma stating`forall 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 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.

of course, thanks !

Last updated: Apr 21 2024 at 01:02 UTC