generalizing deriv to TVS

Stream: maths

[Yury G. Kudryashov]

It seems that I've missed this thread in 2022. I suggest that we redefine docs#fderiv in similar terms. What do you think?

[Yury G. Kudryashov]

@Sebastien Gouezel @Heather Macbeth @Anatole Dedecker :up:

[Yury G. Kudryashov]

We can redefine has_fderiv_at f f' a as ∀ (U ∈ 𝓝 0) (r' ≠ 0) s, is_vonN_bounded 𝕜 s → ∀ᶠ r : 𝕜 in 𝓝[≠] 0, maps_to (λ x, f (a + x) - f a - f' x) (r • s) (r' • r • U) (not tested, may contain typos)

[Yury G. Kudryashov]

BTW, we can redefine topology on multilinear forms in a similar way.

[Yury G. Kudryashov]

Then many facts will work without norms.

[Yury G. Kudryashov]

(though proofs will be harder)

[Moritz Doll]

I think we had a similar discussion before. I am generally in favor of this, however there might be subtleties when it comes to higher derivatives. The only reference for something like this I know is Hamilton's 1982 paper on Nash-Moser theory and he uses directional derivatives and I don't know whether his smoothness is the same as your proposed smoothness (which would make mathlib's smooth Fréchet manifolds weaker).

[Yury G. Kudryashov]

I suggest that the following plan (each step is 1 or more PRs):

1. Drop has_fderiv_at_filter, leave only has_fderiv_within_at and has_fderiv_at (defined as has_fderiv_within_at ... univ).
2. Redefine has_fderiv_within_at for topological vector spaces. Prove equivalence to the old definition, leave all theorems as is.
3. Gradually migrate theorems to topological vector spaces.

[Sebastien Gouezel]

Do you have an application in mind? I have no objection in theory, but I am not sure I see the point yet.

[Eric Wieser]

I have one; I can't talk about derivatives of matrix functions because to even state the results I have to choose a norm

[Yury G. Kudryashov]

This :up: and some other finite dimensional spaces.

[Eric Wieser]

So right now if I wanted to write down how derivatives (by a scalar) distribute across a matrix product, I need to repeat the lemma for every currently-available norm on matrices (I think we have 3 right now via local attribute [instance] and nothing globally)

[Sebastien Gouezel]

Your lemmas should be true for any norm on matrices, so why not write them right away in this generality?

[Yury G. Kudryashov]

What other examples of "canonical topology, no canonical norm" do we have?

[Yury G. Kudryashov]

This came up in a discussion with @Heather Macbeth about tensor products of vector bundles. But in that case there is no canonical topology either.

[Eric Wieser]

Sebastien Gouezel said:

Your lemmas should be true for any norm on matrices, so why not write them right away in this generality?

How do you suggest I state something like

lemma has_deriv_at.matrix_mul (X : R → matrix m n R) (Y : R → matrix n p R)
  (X' : matrix m n R) (Y' : matrix n p R) (r : R)
  (hX : has_deriv_at X X' r) (hY : has_deriv_at Y Y' r) :
  has_deriv_at (λ a, (X a) ⬝ (Y a)) (X' ⬝ Y r + X r ⬝ Y') r :=
begin

[Sebastien Gouezel]

Can you add some typeclasses here? You need some topology somewhere.

[Eric Wieser]

Sure, here's the #mwe, extracted from lean-matrix-cookbook

import analysis.matrix

variables {ι : Type*} {R : Type*} {m n p : Type*}
variables [fintype m] [fintype n] [fintype p]
variables [decidable_eq m] [decidable_eq n] [decidable_eq p]
variables [nontrivially_normed_field R]

open matrix
open_locale matrix

local attribute [instance] matrix.normed_add_comm_group matrix.normed_space

lemma has_deriv_at_matrix {f : R → matrix m n R} {r : R} {f' : matrix m n R} :
  has_deriv_at f f' r ↔ (∀ i j, has_deriv_at (λ r, f r i j) (f' i j) r) :=
by simp_rw has_deriv_at_pi

lemma has_deriv_at.matrix_mul (X : R → matrix m n R) (Y : R → matrix n p R)
  (X' : matrix m n R) (Y' : matrix n p R) (r : R)
  (hX : has_deriv_at X X' r) (hY : has_deriv_at Y Y' r) :
  has_deriv_at (λ a, (X a) ⬝ (Y a)) (X' ⬝ Y r + X r ⬝ Y') r :=
begin
  rw has_deriv_at_matrix at ⊢ hX hY,
  intros i j,
  simp only [mul_apply, pi.add_apply, ←finset.sum_add_distrib],
  exact has_deriv_at.sum (λ k hk, (hX _ _).mul (hY _ _)),
end

[Eric Wieser]

But I cheated, this is only about matrix.normed_space and not the other norms

[Anatole Dedecker]

I’ve spent some time a year ago thinking about how to get meaningful differentiability (which really means a good notion of docs#is_o) without any norm, specifically for the case of finite dimensional vector spaces where we don’t want to impose the norm, but I didn’t think about using docs#is_vonN_bounded for that. This is interesting, do you have any reference ? (Or maybe this is well known and I’m just not aware of it)

[Eric Wieser]

I can't write [normed_add_comm_group (matrix m n R)] [normed_space R (matrix m n R)] because then I get a nonsense addition on the matrices that might not be elementwise

[Sebastien Gouezel]

In this generality, it's definitely not true for all norms (since norms are not all equivalent as you're not assuming your field is complete).

[Sebastien Gouezel]

But I agree I don't see a neat way to write it for all norms even if your field is nice, because normed_add_comm_group can't be expressed with a mixin.

[Sebastien Gouezel]

However, I wouldn't see a way to write it for all topologies either, for the same reason.

[Anatole Dedecker]

One case I’ve heard about a few weeks ago is when you have docs#with_seminorms, then it makes perfect sense to say that docs#is_o means "is_o with respect to each seminorm" and then I think that agrees with the version Yury gave

[Sebastien Gouezel]

Scratch that, for topologies we can definitely use mixins.

[Anatole Dedecker]

For matrices that’s no problem anyway, we have docs#matrix.topological_space

[Yury G. Kudryashov]

Anatole Dedecker said:

I’ve spent some time a year ago thinking about how to get meaningful differentiability (which really means a good notion of docs#is_o) without any norm, specifically for the case of finite dimensional vector spaces where we don’t want to impose the norm, but I didn’t think about using docs#is_vonN_bounded for that. This is interesting, do you have any reference ? (Or maybe this is well known and I’m just not aware of it)

I don't know about references. I just made it up.

[Yury G. Kudryashov]

Possibly, there are better ways to generalize it to topological vector spaces - I don't know.

[Eric Wieser]

Sebastien Gouezel said:

But I agree I don't see a neat way to write it for all norms even if your field is nice, because normed_add_comm_group can't be expressed with a mixin.

I attempted to change it to be a mixin in #18462, but that's lost to the porting tide now (and wasn't looking promising performance-wise)

[Oliver Nash]

I've occasionally mused about generalising fderiv in another direction, where we weaken the module structure on the domain so that the axioms smul_add and add_smul are only required to hold for sufficiently small scalars. The motivation is that the circle (or tori) possess such scalar actions so we could speak of smooth functions on them without having to regard them as manifolds.

[Oliver Nash]

(I'm not seriously suggesting we actually do this.)

[Tomas Skrivan]

Why is deriv defined from a normed field to a normed vector space? For example this wiki article talks about well defined and well behaved derivative from finite dimensional spaces to a general topological vector space. Is this because deriv is defined through fderiv?

---

edit: this was originally the first post in this thread but earlier discussion from a different thread was moved here. Also those two threads got interleaved so it is a bit incoherent right now ...

[Jireh Loreaux]

I think there was a recent discussion about generalizing both, but I'm on mobile so I can't find it now.

[Tomas Skrivan]

A link to such discussion would be appreciated, I did some searching but I couldn't find any relevant discussions.

[Eric Wieser]

Maybe this thread?

[Yury G. Kudryashov]

Probably, we should generalize it but this can't be done before the port is over.

[Tomas Skrivan]

Waiting for the port to be done makes total sense. I was curious what are the thoughts on this topic as I need the generalization for my project.

[Anatole Dedecker]

Since this thread has been linked from somewhere else, I just want to add that the second part of this discussions is not really related to the original topic: unless I’m missing something obvious, the topology on continuous linear maps does not matter here

[Tomas Skrivan]

I initialized the other thread and my motivation for generalizing derivative and differentiability is to allow for isomorphism: $C^\infty(\mathbb{R}^2, \mathbb{R}) \cong C^\infty(\mathbb{R}, C^\infty(\mathbb{R}, \mathbb{R}))$ which requires to define suitable topology on $C^\infty(\mathbb{R}, \mathbb{R})$.

After this is done, I want to do some variational calculus calculations.

[Kevin Buzzard]

What topology are you proposing to put on $C^\infty(\R,\R)$ to make that assertion true?

[Tomas Skrivan]

The topology of uniform convergence on compact sets of each derivative separately, see wiki on convenient vector spaces.

[Tomas Skrivan]

You can define such topology for any locally convex TVS with some mild completeness condition and you have a general isomoprhism $C^\infty(X\times Y, Z) \cong C^\infty(X, C^\infty(Y, Z))$

[Kevin Buzzard]

Oh nice! I could see that it would have to be subtle but I didn't know the answer.

[Tomas Skrivan]

It is kind of messed up because you end up with functions that are differentiable but not continuous.

[Yury G. Kudryashov]

What are your applications?

[Tomas Skrivan]

(deleted)

[Yury G. Kudryashov]

Let me move the second part of this thread to the new one.

[Tomas Skrivan]

I'm working on symbolic and automatic differentiation for SciLean and if I hope to have it verified I need this generalization of derivative.

[Notification Bot]

40 messages were moved here from #maths > Topology on continuous_maps without a norm by Yury G. Kudryashov.

[Yury G. Kudryashov]

Now the history looks a bit strange ;)

[Tomas Skrivan]

ohh well :man_shrugging: I added a small explanation to my first post at least.

[Anatole Dedecker]

To get back to your original question, I think the reason we don't have this easy generalization (talking about deriv here, not fderiv) is indeed because we tend to see deriv as the one-dimensional Fréchet derivative instead of the one-dimensional Gâteaux dérivative. Of course they give the same notion, but because we want the APIs of fderiv and deriv to be similar we probably miss some easy generalizations of deriv.

[Yury G. Kudryashov]

But we can generalize fderiv too (see above)

[Yury G. Kudryashov]

So, the answer is: at the time derivatives were added to mathlib (~4 years ago), nobody cared about this generality.

[Anatole Dedecker]

I agree, my point (and I think Tomas' original message too) was about the fact that the generalization to TVS of deriv is way easier: you can just take the usual limit of (f (x + h) - f x) / h and you don't need any more machinery. But if we make the generalization you suggest (and check that it is indeed a strict generalization of this) then that's even better.

[Tomas Skrivan]

@Yury G. Kudryashov I'm not familiar with von Neumann bounded sets. Do you know the relationship between your suggested generalization and differentiability between convenient vector spaces?

[Yury G. Kudryashov]

What definition are you talking about? I don't know any references on the subject. I made up the definition above in some conversation.

[Yury G. Kudryashov]

Wikipedia says that it is possible to generalize derivatives to TVS "in muliple ways" but doesn't give references.

[Yury G. Kudryashov]

I think that my definition should be equivalent to https://en.wikipedia.org/wiki/Fr%C3%A9chet_derivative#Generalization_to_topological_vector_spaces

[Yury G. Kudryashov]

UPD: my definition is a bit different but should be equivalent for "nice" TVS domains (probably, locally bounded).

[Yury G. Kudryashov]

I guess, we should use the one from Wikipedia instead. UPD: but we need to generalize it to any normed field instead of real numbers.

[Yury G. Kudryashov]

Should we add a version of docs4#Asymptotics.IsLittleO for TVS?

[Yury G. Kudryashov]

We can't generalize this definition becase it doesn't require a vector space structure; some properties work for a normed group.

[Eric Wieser]

image.png

:angry:

[Eric Wieser]

What would the TVS version look like?

[Yury G. Kudryashov]

We need special support for irreducible_def in doc-gen4

[Reid Barton]

Eric Wieser said:

What would the TVS version look like?

Probably it would look the same

[Eric Wieser]

I meant, what would the lean definition look like, not the docs!

[Yury G. Kudryashov]

/me is thinking

[Yury G. Kudryashov]

Not tested:

import Mathlib.Analysis.Asymptotics.Asymptotics

open Set Filter Topology Pointwise

def IsLittleOTVS (𝕜 : Type _) [NontriviallyNormedField 𝕜] {α E F : Type _}
    [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E]
    [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F]
    (f : α → E) (g : α → F) (l : Filter α) : Prop :=
    ∀ V ∈ 𝓝 (0 : F), ∃ U ∈ 𝓝 (0 : E), ∃ (φ : α → ℝ), Tendsto φ l (𝓝[>] 0) ∧
      ∀ᶠ x in l, ∀ a b : 𝕜, ‖a‖ ≤ φ x * ‖b‖ → g x ∈ b • V → f x ∈ a • U

[Yury G. Kudryashov]

Trying to prove

theorem isLittleOTVS_iff_isLittleO (𝕜 : Type _) [NontriviallyNormedField 𝕜] {α E F : Type _}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
    {f : α → E} {g : α → F} {l : Filter α} :
    IsLittleOTVS 𝕜 f g l ↔ f =o[l] g := by

[Yury G. Kudryashov]

This :up: definition is wrong. Thinking.

[Yury G. Kudryashov]

You can always take U = univ

[Yury G. Kudryashov]

(no, you can almost always take a = 0 to fail the definition)

[Tomas Skrivan]

Yury G. Kudryashov said:

What definition are you talking about? I don't know any references on the subject. I made up the definition above in some conversation.

I would say that f : E → F is differentiable at x if for every curve γ : 𝕜 → E differentiable at 0 and γ 0 = x the curve f ∘ γ : 𝕜 → F is differentiable at 0.

Is that reasonable generalization? If you require smoothness in the definition then based on wiki this should recover any reasonable definition of smoothness for Frechet spaces.

[Yury G. Kudryashov]

This is not a generalization of Frechet derivative.

[Yury G. Kudryashov]

For a normed vector space, it is not equivalent to docs4#HasFDerivAt

[Tomas Skrivan]

I see, then I do not understand these things properly. Why is not equivalent? Is there a counter example?

[Yury G. Kudryashov]

The problem is with "if you require smoothness"

[Yury G. Kudryashov]

First of all, your definition does not involve any continuous linear map.

[Yury G. Kudryashov]

I think that $f(x, y)=\frac{x^3}{x^2+y^2}$ is differentiable at zero in the sense of curves but it is not Frechet differentiable.

[Tomas Skrivan]

Ahh right, it is mentioned here https://ncatlab.org/nlab/show/Boman%27s+theorem

My final suggestion would be:
f : E → F is differentiable at x if for every γ : 𝕜×𝕜 → E differentiable at 0 and γ 0 = x the f ∘ γ : 𝕜×𝕜 → F is differentiable at 0.

but I really do not understand these things in depth, so I should stop suggesting anything further :)

[Yury G. Kudryashov]

I proved that the following:

import Mathlib.Analysis.Asymptotics.Asymptotics
import Mathlib.Analysis.SpecificLimits.Basic

open Set Filter Topology Pointwise Asymptotics Metric

section TVS

variable  (𝕜 : Type _) [NontriviallyNormedField 𝕜] {α E F : Type _}
    [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E]
    [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F]

def IsLittleOTVS (f : α → E) (g : α → F) (l : Filter α) : Prop :=
  ∀ U ∈ 𝓝 (0 : E), ∃ V ∈ 𝓝 (0 : F), ∀ c : ℝ, 0 < c →
    ∀ᶠ x in l, ∀ b : 𝕜, b ≠ 0 → g x ∈ b • V → ∃ a : 𝕜, ‖a‖ ≤ c * ‖b‖ ∧ f x ∈ a • U

end TVS

theorem isLittleOTVS_iff_isLittleO (𝕜 : Type _) [NontriviallyNormedField 𝕜] {α E F : Type _}
    [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
    {f : α → E} {g : α → F} {l : Filter α} :
    IsLittleOTVS 𝕜 f g l ↔ f =o[l] g := by
  _

The proof is in branch4#YK-isO-TVS

[Anatole Dedecker]

@Tomas Skrivan We will definitely need to have different higher-dimensional-domain derivatives at some point (or rather of differentiability I guess, since when they are defined they all agree) anyway, the key point being that fderiv should keep being the usual one in the case of normed spaces. That said, I would guess and hope that we can stay with only one version in the case of one dimensional domain.

[Tomas Skrivan]

One thing I do not understand is what is the motivation to have Frechet derivative as the base definition? If a function has Frechet derivative then it has Gateaux derivative. Why not have Gateaux derivative as the basic definition and have theorem that on nice spaces and under nice differentiability conditions it is Frechet derivative.

[Sebastien Gouezel]

You want a notion that has nice properties, in the sense that it makes it possible to prove nice theorems. For instance the local inverse theorem, which says that if the derivative is invertible then the map is locally invertible. Or the implicit function theorem. These are true for the Fréchet derivative, but not for the Gateaux derivative. In a sense, Gateaux derivative is a nice gadget, but not useful to prove theorems. While Fréchet derivative is the fundamental notion.

[Eric Wieser]

Wikipedia says:

If F is Fréchet differentiable, then it is also Gateaux differentiable, and its Fréchet and Gateaux derivatives agree

If this is actually true in general and not just for the cases wikipedia cares about, then presumably the answer to "Why not have Gateaux derivative as the basic definition" is "it's convenient to have the derivative fderiv bundled as a multilinear map"?

[Sebastien Gouezel]

You could have a definition of a derivative as "if there is a continuous linear map which gives the directional derivative in every direction, then use it, and otherwise take 0". This would be the Gateaux derivative in mathlib conventions. And it would be essentially useless because it doesn't have nice properties without further assumptions which amount to saying that the function is in fact Fréchet-differentiable. For instance, a function which is Gateaux-differentiable at a point doesn't have to be continuous there. Or, the composition of two Gateaux-differentiable maps is not in general Gateaux-differentiable. It's just a bad notion from the mathematical point of view.

[Yury G. Kudryashov]

Inverse theorem needs strict differentiability, not only Fréchet.

[Yury G. Kudryashov]

You can define Gateaux derivative using Fréchet:

def HasDirDerivAt (f : E → F) (f' : F) (v x : E) : Prop :=
  HasDerivAt (f ∘ lineMap x (v + x) : 𝕜 → F) f' 0

def dirDeriv (f : E → F) (v x : E) : F :=
  deriv (f ∘ lineMap x (v + x) : 𝕜 → F) 0

def GateauxDifferentiableAt (f : E → F) (x : E) : Prop :=
  ∀ v, DifferentiableAt 𝕜 (f ∘ lineMap x (v + x) : 𝕜 → F) 0

[Tomas Skrivan]

I think the only thing I'm suggesting is to have deriv and it's bundled version fderiv as general as possible and then of course have theorems about them with different notions of differentiability.

I would like to formalize Convenient Vector spaces, define a new notion of differentiability and reuse mathlib's deriv but I can't do that as it is restricted to normed spaces.

[Sebastien Gouezel]

This is a very niche and exotic notion. Are you sure you really need that for your formalization, instead of sticking with more mainstream and established mathematics?

[Tomas Skrivan]

I want to formalize computations in variational calculus, in particular calculations commonly done by physicists in mechanics or thermodynamics.

Using lebesgue/sobolev spaces is annoying as you have to deal with integrability which is completely unrelated to why you would do those computations.

I really want to work with smooth functions, but they do not behave well w.r.t. standard notions of vector spaces.

That is why I want to use convenient vector spaces, I get smooth functions and cartesian closed category which simplifies lot of arguments.

[Yury G. Kudryashov]

@Tomas Skrivan Once we generalize Fréchet derivatives, you can define Gateaux derivatives as above, if you need them.

[Yury G. Kudryashov]

What do we need to assume about topology on the (co)domain to have IsLittleOTVS.add? The problem is that we can choose different as.

[Jireh Loreaux]

If 𝕜 were ℝ there would be no problem right? Because then if you get a₁ and a₂ for the individuals, you can take a := ∥a₁∥ + ∥a₂∥ for the sum. Just trying to make sure I understand the issue. (In my head the problem isn't that you have two as, it's that you don't know how to make them "point in the same direction")

[Yury G. Kudryashov]

Yes.

[Yury G. Kudryashov]

Probably, we should require that nhds of zero has a basis of docs4#Balanced sets.

[Jireh Loreaux]

It's still not clear how to pick a though.

[Jireh Loreaux]

Because you could have say a₁ = (1 : ℂ) and a₂ = Complex.I.

[Yury G. Kudryashov]

I think that Balanced should fix this but I don't have time now. Maybe, tomorrow.

[Anatole Dedecker]

Yury G. Kudryashov said:

Probably, we should require that nhds of zero has a basis of docs4#Balanced sets.

This is always true, see docs4#nhds_basis_balanced

[Anatole Dedecker]

I haven't spent enough times thinking about this to be sure about what I say, but I think that another reasonable definition would be the following:

import Mathlib.Analysis.Asymptotics.Asymptotics
import Mathlib.Analysis.SpecificLimits.Basic
import Mathlib.Analysis.Convex.Gauge

open Set Filter Topology Pointwise Asymptotics Metric
open scoped ENNReal

section TVS

variable  (𝕜 : Type _) [NontriviallyNormedField 𝕜] {α E F : Type _}
    [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E]
    [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F]

-- I would argue this should be the general replacement for `gauge`, but I could be wrong
noncomputable def gauge' (s : Set E) (x : E) : ℝ≥0∞ := sInf ((↑‖·‖₊) '' {k : 𝕜 | x ∈ k • s})

def IsLittleOTVS (f : α → E) (g : α → F) (l : Filter α) : Prop :=
  ∀ U ∈ 𝓝 (0 : E), ∃ V ∈ 𝓝 (0 : F), ∀ (c : ℝ≥0∞), 0 < c → ∀ᶠ x in l, (gauge' 𝕜 U (f x)) ≤ c * (gauge' 𝕜 V (g x))

I am pretty confident that this gives the usual version in normed spaces, but not sure that it's the same notion as Wikipedia's or Yury's. The reason this feels natural is that, if topologies on E and F are generated by seminorms, I think you get a nice-looking characterization, but it's getting too late to even state it...

[Anatole Dedecker]

See docs4#gauge and the whole file around it. In particular, the gauge (or gauge’) of the unit ball of a normed space is exactly the norm

[Yury G. Kudryashov]

1. I think that your gauge' should be added as egauge to the library, similar to edist. gauge should be redefined as (egauge _ _).toReal.
2. I think that our definitions are equivalent. I didn't use docs#gauge in mine because it's not egauge.

[Yaël Dillies]

So you lose the fact that the gauge returns a scalar?

[Kevin Buzzard]

In the p-adic theory Frechet spaces are topological vector spaces whose topology is defined by a family of seminorms and they play a big role in the p-adic Langlands program. I'm assuming this is material that we stole from the real analysts...

[Yury G. Kudryashov]

Yaël Dillies said:

So you lose the fact that the gauge returns a scalar?

Currently, gauge is only defined for a real vector space.

[Anatole Dedecker]

I’m on mobile right now so I won’t develop all of my thoughts, but there are two distinct deviations from gauge at play.

• The first one is indeed just a matter of taking values in ENNReal instead of Real. I would say we should definitely keep both
• The other one is that, even where both the infimum is well defined, it’s not clear that the two agree for a non-symmetric set. On the other hand, I see no way to generalize gauge to arbitrary field that would preserve this property. This reminds me of the "real polar" VS "absolute polar" design choice, and iirc we chose the latter precisely because it works over other fields

[Anatole Dedecker]

Hence I have a question for people more familiar with convex analysis: do you care about the value of the gauge for non absorbent and balanced sets ?

[Yury G. Kudryashov]

@Brendan Seamas Murphy does to construct a homeomorphism with a ball.