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

#### 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: Dec 20 2023 at 11:08 UTC