Normed linear ordered field

Stream: general

[Yaël Dillies]

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]

cc @Anatole Dedecker

[Reid Barton]

Yaël Dillies said:

• defining linear_ordered_nondiscrete_normed_field

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

[Reid Barton]

which I think is already linear_ordered_field right?

[Yaël Dillies]

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]

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]

(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]

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

[Yaël Dillies]

Oh, docs#linear_ordered_field.to_densely_ordered

[Reid Barton]

I agree an ordered field with a norm isn't necessarily nondiscrete in the sense of mathlib

[Yaël Dillies]

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]

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

[Reid Barton]

How does this type check? Isn't b : 𝕜 while dist x z : real

[Yaël Dillies]

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]

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]

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]

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

[Jireh Loreaux]

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]

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]

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]

And how do I state that? normed_algebra ℝ 𝕜?

[Reid Barton]

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