# Zulip Chat Archive

## Stream: general

### Topic: Normed linear ordered field

#### Yaël Dillies (Apr 15 2022 at 14:54):

In #13379 I (think I) need a dense normed linear ordered field. What do people think of either

- defining
`linear_ordered_nondiscrete_normed_field`

- adding
`non_trivial : ∃ (x : α), 1 < ∥x∥`

to docs#normed_linear_ordered_field. As the only two instances are`ℚ`

and`ℝ`

, this wouldn't change anything (~~but it would indeed exclude possible candidates, like $\{-1, 0, 1\}$~~)

#### Yaël Dillies (Apr 15 2022 at 14:54):

cc @Anatole Dedecker

#### Reid Barton (Apr 15 2022 at 14:58):

Yaël Dillies said:

- defining
`linear_ordered_nondiscrete_normed_field`

Is this the same as https://en.wikipedia.org/wiki/Ordered_field?

#### Reid Barton (Apr 15 2022 at 15:00):

which I think is already `linear_ordered_field`

right?

#### Yaël Dillies (Apr 15 2022 at 15:00):

Are you saying that docs#normed_linear_ordered_field.to_normed_field should instead be `normed_linear_ordered_field.to_nondiscrete_normed_field`

?

#### Reid Barton (Apr 15 2022 at 15:03):

Oh I think I'm confused about this norm business. In my world if you are regarding K-vector spaces as having a "norm" (K being an ordered field) then the "norm" should take values in K not the reals.

#### Reid Barton (Apr 15 2022 at 15:08):

(e.g. the norm on $K$ itself is given by $||a|| = |a|$ and it's automatically "nondiscrete" in whatever sense you like, because $K$ is dense as an ordered set)

#### Yaël Dillies (Apr 15 2022 at 15:09):

Does ìt have to be dense? Do we have that?

#### Yaël Dillies (Apr 15 2022 at 15:09):

Oh, docs#linear_ordered_field.to_densely_ordered

#### Reid Barton (Apr 15 2022 at 15:10):

I agree an ordered field with a norm isn't necessarily `nondiscrete`

in the sense of mathlib

#### Yaël Dillies (Apr 15 2022 at 15:12):

I'm still not sure this answers my original enquiry. The question is for what `something`

this holds true

```
import analysis.normed_space.pointwise
variables {𝕜 E : Type*} [something 𝕜] [normed_space 𝕜 E] {δ ε : 𝕜}
lemma exists_dist_eq (x z : E) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
∃ y, dist x y = b * dist x z ∧ dist y z = a * dist x z := sorry
lemma exists_dist_lt_lt (hδ : 0 < δ) (hε : 0 < ε) (h : dist x z < ε + δ) :
∃ y, dist x y < δ ∧ dist y z < ε :=
```

#### Reid Barton (Apr 15 2022 at 15:13):

Probably a natural condition relating the ordering and the norm is that the norm should be convex (over $K$)

#### Reid Barton (Apr 15 2022 at 15:14):

How does this type check? Isn't `b : 𝕜`

while `dist x z : real`

#### Yaël Dillies (Apr 15 2022 at 15:14):

Yeah we need a coercion from `𝕜`

to `ℝ`

. This is why I only stated it for `ℝ`

so far, but left a comment saying it could be stated for `ℚ`

.

#### Yaël Dillies (Apr 15 2022 at 15:15):

So far we have docs#convex_on_norm. But those results are hard to get in general because you usually can't relate `a + b = 1`

and `∥a∥ + ∥b∥ = 1`

. I believe docs#normed_algebra does help here.

#### Jireh Loreaux (Apr 15 2022 at 15:19):

Aside from looking unnatural, is there a reason you couldn't just use `∥a∥`

, `∥b∥`

in place of `a`

, `b`

(this would also solve the coercion problem)? This is probably not the right choice, but I'm not really clear what your end goal is.

#### Yaël Dillies (Apr 15 2022 at 15:20):

Probably looking through #13379 will be the fastest way to understand my motivation.

#### Jireh Loreaux (Apr 15 2022 at 15:20):

For clarity:

```
lemma exists_dist_eq (x z : E) {a b : 𝕜} (hab : ∥a∥ + ∥b∥ = 1) :
∃ y, dist x y = ∥b∥ * dist x z ∧ dist y z = ∥a∥ * dist x z := sorry
```

#### Yaël Dillies (Apr 15 2022 at 15:23):

My general goal is showing that balls of radius `r`

contain elements of distance arbitrarily close to `r`

in all directions. This implies in particular that two balls are disjoint iff the sum of their radii is less than the distance between their center (#13379), that thickening by `δ`

then thickening by `ε`

is the same as thickening by `δ + ε`

(#13380), that adding a ball of radius `δ`

to a ball of radius `ε`

gives a ball of radius `δ + ε`

(#13381)...

#### Reid Barton (Apr 15 2022 at 15:25):

In the form with real-valued norms I think this only makes sense for $K$ a subfield of the reals, with the induced norm--is that what you had in mind?

#### Yaël Dillies (Apr 15 2022 at 15:29):

And how do I state that? `normed_algebra ℝ 𝕜`

?

#### Reid Barton (Apr 15 2022 at 15:31):

Well they are also the archimedean ordered fields but I'm not sure that helps directly.

Last updated: Aug 03 2023 at 10:10 UTC