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.

[Yury G. Kudryashov]

#12852 is a step towards derivatives for functions between TVS

[Eric Wieser]

Just to check, are there any open PRs currently on the path to this?

[Yury G. Kudryashov]

There is a draft PR #9675 which defines IsLittleOTVS and proves both equivalences we care about (to IsLittleO for normed spaces and to "tends to zero" for domain = field).

[Yury G. Kudryashov]

The main issue with this PR is it has low priority for me. If you want to take over it, then you're welcome.

[Yury G. Kudryashov]

Once we have it, we can define HasFDerivAtFilter for a topological vector space, but prove everything for normed spaces.

[Yury G. Kudryashov]

Of course, later we may decide to generalize some proofs to TVS.

[Yury G. Kudryashov]

Also, #15217 is a bit related (it's used in WIP #13648 which generalized docs#ContinuousLinearMap.compSL to TVS, not 100% sure that we'll need it, but seems relevant).

[Eric Wieser]

Yury G. Kudryashov said:

The main issue with this PR is it has low priority for me. If you want to take over it, then you're welcome.

I've fixed the conflicts and new lint warnings, but it seems there is a gap in the proof

[Yury G. Kudryashov]

I'll fix it today. AFAIR, I wrote the proof w/o egauge, then partially migrated to egauge.

[Yury G. Kudryashov]

Fixed, pushed

[Yury G. Kudryashov]

#9675 is ready for review!

[Eric Wieser]

The details are slightly above my paygrade, but this seems clearly useful for generalizing HasDerivAt etc. Does anyone else more qualified (@Anatole Dedecker, @Sébastien Gouëzel?) want to review, or should we just put this in?

[Eric Wieser]

#19104 is the next piece towards generalizing the definitions

[Eric Wieser]

And now the very trivial #19114

[Eric Wieser]

#19108 is the main change, though bizarrely this fails because the elaborator now thinks it has to find NormedAddCommGroup (List 𝔸)

[Eric Wieser]

Any more thoughts on #19108?

[Kevin Buzzard]

My thoughts are "golly, lots of files are now slower"

[Patrick Massot]

Yes, this is really worrying. Do we know how much time this actually represents? Are those big files?

[Junyan Xu]

If you look at the bench results (unfortunately the bench summary bot is dead now), you see that build is 0.359% slower, which is equivalent to adding 20.6 files or 6k lines to mathlib. Lint is 0.394% slower but only costs ~5% instructions compared to build.

[Junyan Xu]

I see that Mathlib.Analysis.Calculus.Deriv.Prod got 102% slower though. Probably worth investigating ...

[Eric Wieser]

By wall clock, the total build is 0.6% or 6s slower, where the current build time is 17 minutes and 15 seconds

[Eric Wieser]

I investigated the file with the largest absolute slowdown using the firefox profiler; my takeaway is that statements like HasDerivAt f f' take longer to elaborate because before the process was:

• I need NormedAddCommGroup F
• Oh, it's in the context

and now its:

• I need AddCommGroup F
• I will do a typeclass search
• Goose chasing ensues
• Oh, it's NormedAddCommGroup.toAddCommGroup

and this happens for every single reference to these definitions.

[Kevin Buzzard]

I see! And we definitely don't want to increase the priority of NormedAddCommGroup.toAddCommGroup because 99% of the time this is a disastrous thing to try (leading us on a wild goose chase) and the right answer is probably Ring.toAddCommGroup.

[Eric Wieser]

A reasonable stance to hold would be "pick any priorities you like if mathlib becomes faster as a result" but this of course has unpredictable impact on code that hasn't been written yet

[Eric Wieser]

I think the performance hit for Prod specfically can be greatly reduced in future by generalizing the lemmas to also not need NormedAddCommGroup at all

[Eric Wieser]

But this a) is a massive scope creep, and b) probably just shifts the performance drop to the callers, where the game can maybe be repeated in exchange for even further scope creep

[Eric Wieser]

Kevin Buzzard said:

golly, lots of files are now slower"

Perhaps also worth considering that the push for file splits / the overall growth of mathlib is going to mean that performance issues increasingly impact "lots" of files

[Junyan Xu]

Maybe refreshing the NormedAddCommGroup.toAddCommGroup instance locally would help. I've noticed that once you import Nat.card etc. into the algebraic hierarchy (e.g. in Ideal/Quotient/Operations), the trace for synthesizing CommRing.toRing becomes this:

[Meta.synthInstance] :check: Ring R ▼
[] new goal Ring R ▶
[] :check: apply @StrictOrderedRing.toRing to Ring R ▶
[] :check: apply @LinearOrderedRing.toStrictOrderedRing to StrictOrderedRing R ▶
[] :check: apply @LinearOrderedCommRing.toLinearOrderedRing to LinearOrderedRing R ▶
[] :check: apply @LinearOrderedField.toLinearOrderedCommRing to LinearOrderedCommRing R ▶
[] :check: apply @StrictOrderedCommRing.toStrictOrderedRing to StrictOrderedRing R ▶
[] :check: apply @LinearOrderedCommRing.toStrictOrderedCommRing to StrictOrderedCommRing R ▶
[] :check: apply @OrderedRing.toRing to Ring R ▶
[] :check: apply @OrderedCommRing.toOrderedRing to OrderedRing R ▶
[] :check: apply @StrictOrderedCommRing.toOrderedCommRing to OrderedCommRing R ▶
[] :check: apply @StrictOrderedRing.toOrderedRing to OrderedRing R ▶
[] :check: apply @DivisionRing.toRing to Ring R ▶
[] :check: apply @Field.toDivisionRing to DivisionRing R ▶
[] :check: apply @LinearOrderedField.toField to Field R ▶
[] :check: apply @CommRing.toRing to Ring R ▶
[] :check: apply inst✝¹ to CommRing R ▶
[resume] propagating CommRing R to subgoal CommRing R of Ring R ▶
[] result CommRing.toRing

However, refreshing the CommRing.toRing instance has a mixed effect: it makes some decls in the file faster and some slower.

[Kevin Buzzard]

As you may well know, unfolding the new goal Ring R ▶ line in your trace shows the list of instances which Lean is about to apply in reverse order in order to try and solve Ring R. The list is ordered by priority, with things of equal priority being ordered by when Lean found them, so in particular out of all of the things with default priority, it tries the one it learnt last, first.

[Eric Wieser]

I'll use this as an opportunity to suggest people upvote lean4#6389, since without that the infoview doesn't reveal that LinearOrderedField.toField is a subgoal generated by DivisionRing.toRing

[Kevin Buzzard]

(I noticed that this had changed in the infoview, and just assumed that it was intentional because I barely ever look at the command line output)

[Junyan Xu]

so in particular out of all of the things with default priority, it tries the one it learnt last, first.

Yes I'm aware, and by "refreshing" I mean just reiterate an existing instance again to ensure it's fresh in Lean's memory (as if it just learnt it).

[Junyan Xu]

I also tried to lower the priority of StrictOrderedRing.toRing etc. here but then something in Mathlib/Tactic/Positivity/Core.lean times out.

[Kevin Buzzard]

Yes it seems to me that the moment you start globally goofing around, you break random unrelated files. One hack might be to locally fudge priorities in the files which are currently slower?

[Michael Stoll]

This is likely related to the order+algebra type class problem that I was trying to mitigate in #12778 ...

[Kevin Buzzard]

Yes, I guess this is the related norm+algebra typeclass problem :-/

[Eric Wieser]

The norm+algebra one is arguably worse because we inherited a weird mix of new- and old- style classes from Lean 3

[Eric Wieser]

But I'd rather that we not gate the titular generalization in #19108 that costs a 6s global slow down on a multi-month refactor!

[Yury G. Kudryashov]

BTW, we use very different approaches to topological groups and normed groups. For topological groups, it's [AddCommGroup G] [TopologicalGroup G], while normed groups are bundled.

[Yury G. Kudryashov]

Are pros and cons of these approaches described somewhere?

[Yury G. Kudryashov]

Also, we use NormedSpace K E, if K is a field but module+mixins in case K is a normed (division) ring.

[Anatole Dedecker]

Yes, I think that part of the library deserves some technical decisions to be re-evaluated

[Yuyang Zhao]

There was a relevant refactor !3#18462. But it was abandoned for porting.

[Kevin Buzzard]

I'm trying to make some sense of the slowdowns. The first thing to say is that this is nothing like the algebra slowdowns we've seen in the past, where Module \u A B is incredibly slow and you have to bump up max heartbeats to 400,000. These "30% slower files" are still compiling in just a few seconds, it's just that apparently they were compiling in one or two fewer seconds before. Having looked at a random sample of these files I am now far less concerned about merging this PR.

One thing I noticed when experimenting is that whilst it's difficult to put your finger on what is causing the slowdowns (everything is just a bit slower), a random typeclass instance trace in one file has this on master

 [Meta.synthInstance] [0.000128] 💥️ Semiring ?m.340822

and this (for the same search) on the branch

[Meta.synthInstance] [0.000128] 💥️ Semiring ?m.420469

So (looking at the numbers) Lean is is using 25% more metavariables in the branch. I have no idea if this is significant. But what I do know is that these huge percentage increases seem to be completely insignificant in terms of wall clock time so, as I said, I'm very happy to merge. Are there any dissenting voices?

[Kevin Buzzard]

Patrick Massot said:

Yes, this is really worrying. Do we know how much time this actually represents? Are those big files?

These are fast files and they're still fast after this PR. There seems to be little to worry about here.

[Yury G. Kudryashov]

Yuyang Zhao said:

There was a relevant refactor !3#18462. But it was abandoned for porting.

What's known about pros and cons of each approach?

[Junyan Xu]

The slowdown from #19046 and my #17930 are of a similar order (several seconds).

Any one knows why lint uses ~5% instructions as build but ~1/3 wall-clock time? Less parallelization?

[Eric Wieser]

I think lint has basically no parallelization?

[Yury G. Kudryashov]

Why linter can't run itself on all defs/theorems in parallel?

[Yury G. Kudryashov]

Is it "because nobody added this functionality" or there are some obstacles?

[Johan Commelin]

I think that if #17930 now has a slowdown in the range of several seconds, then that is a very acceptable price to pay for generalizing a bunch of stuff to two-sided ideals.

[Junyan Xu]

Thanks! Apparently the slowdown from #17930 is 6.562s (in this run), a bit higher than 5.861s for Eric's #19108, even though in terms of instructions it's 0.178% vs. 0.359%. I guess parallelization and fluctuation are playing a role here.
image.png
image.png

[Eric Wieser]

On the topic of the original thread, #20220 (edit: now depends on #20305) is a step towards generalizing more results to TVSs

[Eric Wieser]

Beyond that, I think the key missing piece is IsLittleOTVS.add, which I think will require something along the lines of

-- probably needs `Convex _ s` and `Absorbent _ s`
lemma egauge_add_le (x y : E) :
    egauge 𝕜 s (x + y) ≤ egauge 𝕜 s x + egauge 𝕜 s y := by

to match docs#gauge_add_le. From there, I can prove (in #20250)

lemma IsLittleOTVS.add
    [TopologicalAddGroup F] [Module ℝ F] [LocallyConvexSpace ℝ F]
    [TopologicalAddGroup E] [Module ℝ E] [LocallyConvexSpace ℝ E]
    {f₁ f₂ : α → E} {g : α → F} {l : Filter α}
    (hf₁ : IsLittleOTVS 𝕜 f₁ g l) (hf₂ : IsLittleOTVS 𝕜 f₂ g l) :
    IsLittleOTVS 𝕜 (f₁ + f₂) g l := by

though having to assume that E is both a 𝕜-vector space and an ℝ-vector space is a little annoying

[Yury G. Kudryashov]

We definitely want HasDerivAt.add to work for fields that aren't RCLike.

[Yury G. Kudryashov]

#34127 generalizes most of the theory about tangentConeAt and UniqueDiffOn to topological vector spaces, changing the definition to

universe u v
variable (R : Type u) {E : Type v}

section TangentConeAt

variable [AddCommMonoid E] [SMul R E] [TopologicalSpace E] {s : Set E} {x y : E}

/-- The set of all tangent directions to the set `s` at the point `x`. -/
def tangentConeAt (s : Set E) (x : E) : Set E :=
  {y : E | ClusterPt y ((⊤ : Filter R) • 𝓝[(x + ·) ⁻¹' s] 0)}

As a side effect, docs#posTangentConeAt becomes a special case of tangentConeAt. Suggestions are welcome. E.g., I'm not sure about 𝓝[(x + ·) ⁻¹' s] 0 vs (𝓝[s] x).comap (x + ·) vs (𝓝[s] x).map (· - x). All three are equivalent in a topological group, so this only affects [ContinuousAdd E] assumptions here and there. Also, should I use [AddCommMonoid E] in the definition and in lemmas that work with this assumption, or stick to at least AddCommGroup E everywhere?

[Yury G. Kudryashov]

I'm reviving an old thread. For those who didn't follow this refactor, we've already generalized HasFDerivAt etc to topological vector spaces, but lots of lemmas still assume NormedSpace.

[Eric Wieser]

Unless we're certain the generality is correct for AddCommMonoid, I'd be inclined to stick with groups for now; that is, focus on just one part of the generalization at a time

[Yury G. Kudryashov]

Which of the three spellings look more natural to you?

[Eric Wieser]

𝓝[(x + ·) ⁻¹' s] 0 has the advantage that when you unfold to it, you don't duplicate x

[Eric Wieser]

I'd like to let @Sébastien Gouëzel have one more look at #34127, but I think it's pretty much ready to go.

[Eric Wieser]

What's the next step after this; is it just mindless typeclass generalization, or is there more mathematical work to do?

[Yury G. Kudryashov]

I think that for fderiv, it's mostly typeclass generalization. If we want to generalize stuff like fderiv_mul to topological algebras over a normed field, then we should replace docs#IsBoundedBilinearMap with a version for topological spaces (a bilinear map that is continuous as a function on the product).

[Yury G. Kudryashov]

For iterated derivatives, the situation is more complicated, because uncurrying only works for normed spaces. Probably, we can generalize to the codomain being a TVS, but not for the domain.

[Eric Wieser]

Do you have a branch already with those generalizations (say, for add and sum), or do you want me to have a go once the above lands?

[Yury G. Kudryashov]

I would wait with this until we generalize enough of theorems about docs#fderiv.

[Yury G. Kudryashov]

I don't have a branch yet.

[Yury G. Kudryashov]

I've recently found out about this approach to $C^k$. I don't know how exactly it relates to our definition in case of real normed spaces.

[Yury G. Kudryashov]

Pros of this approach is that (a) it works for functions on topological vector fields over topological fields (do people really need topological fields w/o a norm? idk); (b) it gives, e.g., symmetry of derivatives over other fields.

[Yury G. Kudryashov]

(c) it looks similar to Whitney differentiability, not sure if it's exactly the same for, e.g., closed sets in finite dimensional spaces.

[Yury G. Kudryashov]

BTW, do you have any idea about why do we see so much red in the benchmark?

[Yury G. Kudryashov]

E.g., would it be better if I assume a stronger typeclass about the coefficients type everywhere? I doubt that we'll need it for anything less than a DivisionSemiring.

[Yury G. Kudryashov]

This will shorten the path in instance searches, but add more fields for defeq calls.

[Yury G. Kudryashov]

BTW, I would appreciate reviews of #34033 and #34074 (more API about asymptotics in TVS).

[Eric Wieser]

Does docs#HasFDerivAtFilter.tendsto_nhds generalize without much work?

[Yury G. Kudryashov]

I might have it in a branch.

[Yury G. Kudryashov]

Let me have a look later today.

[Yury G. Kudryashov]

As for the next few lemmas, I think that we should introduce IsEquivalentTVS. Before doing this, I would prefer to merge the two PRs above, then split the file while moving it to Topology/Algebra/Module/Asymptotics/*.

[Yury G. Kudryashov]

Then I would deprecate the *BigO_*_rev lemmas and replace them with more precise IsEquivalent + IsTheta lemmas.

[Yury G. Kudryashov]

One more unrelated generalization I was thinking about is to make docs#HasFDerivAtFilter take a filter on the product as an argument, so that it works for docs#HasStrictFDerivAt too.

[Eric Wieser]

Eric Wieser said:

Do you have a branch already with those generalizations (say, for add and sum), or do you want me to have a go once the above lands?

#34345 makes a start on basic; I've just commented things out for now to make conflicts easier to resolve

[Eric Wieser]

My guess would be that we should relocate all the commented out code to a new section or file, since the statements actually need a norm in their assumptions or conclusions

[Yury G. Kudryashov]

I can have a look tomorrow.

[Stepan Nesterov]

Yury G. Kudryashov said:

Pros of this approach is that (a) it works for functions on topological vector fields over topological fields (do people really need topological fields w/o a norm? idk); (b) it gives, e.g., symmetry of derivatives over other fields.

I don't think I know any application of talking about merely C^k functions over fields other than R or C. The only regularity class for functions over Q_p I see people work with is analytic functions, where things like symmetry of partials is completely obvious anyway.

[Eric Wieser]

Eric Wieser said:

Does docs#HasFDerivAtFilter.tendsto_nhds generalize without much work?

I worked this one out (edit: #34347)

[Yury G. Kudryashov]

Stepan Nesterov said:

Yury G. Kudryashov said:

Pros of this approach is that (a) it works for functions on topological vector fields over topological fields (do people really need topological fields w/o a norm? idk); (b) it gives, e.g., symmetry of derivatives over other fields.

I don't think I know any application of talking about merely C^k functions over fields other than R or C. The only regularity class for functions over Q_p I see people work with is analytic functions, where things like symmetry of partials is completely obvious anyway.

The paper I've linked shows that at least some people care about ways to define $C^k$ over $\mathbb Q_p$ to get meaningful results. I have no idea how common is it. If this definition is equivalent to Whitney differentiability for closed subsets of $\mathbb R^n$, then I would introduce it. Otherwise, I would wait until one of the people who care about this comes to us.

[Stepan Nesterov]

Sure some people will study it just because they find it intrinsically interesting. I'm just saying that from what I know, there isn't really any use for the C^k-differentiable p-adic functions in mainstream number theory. So if there are some complications with the definition because what if it doesn't work over some crazy fields, I would personally vote for restricting the theory to R or C over doing something very complicated.

[Moritz Doll]

Yury G. Kudryashov said:

For iterated derivatives, the situation is more complicated, because uncurrying only works for normed spaces. Probably, we can generalize to the codomain being a TVS, but not for the domain.

The iterated Frechet derivative for the codomain being a TVS would be amazing to have! I have a bunch of results that I could probably prove very easily, but not state because that is missing.

[Yury G. Kudryashov]

Do you know what definition is the right one in this context? I've misread "codomain" as "domain" :man_facepalming:

[Eric Wieser]

Eric Wieser said:

My guess would be that we should relocate all the commented out code to a new section or file, since the statements actually need a norm in their assumptions or conclusions

Done in #34348.

[Robert Maxton]

I'm someone who would care about "fields other than $\mathbb{R}$ or $\mathbb{C}$"! Specifically I care about (continuous, nonanalytic but presumably smooth functions on) the field of unitary operators on $\mathbb{R}^n$ or $\mathbb{C}^n$, where $n \to \infty$; I'm interested in TVS's because they show up in some approaches to algebraic quantum field theory. I have no idea if that meaningfully changes your constraints any, but since it came up...

[Yury G. Kudryashov]

Are you interested in this field as a field of coefficients or as the domain/codomain of functions?

[Yury G. Kudryashov]

I know there are people here who do analysis with $\mathbb R$, $\mathbb C$, or $\mathbb Q_p$ as the field of scalars. I don't know if people are interested in other fields as fields of scalars. Also, I don't know if there are people here who care about $C^k$ functions, $k<\omega$, in case of the $p$-adic analysis.

[Robert Maxton]

Yury G. Kudryashov said:

Are you interested in this field as a field of coefficients or as the domain/codomain of functions?

Both, but particularly the latter.

[Moritz Doll]

Yury G. Kudryashov said:

Do you know what definition is the right one in this context? I've misread "codomain" as "domain" :man_facepalming:

There is something with derivatives in "tame" Fréchet spaces (grading of the seminorms and some additional condition)- it is some paper by Hamilton. It defines only directional derivatives and C^1 is all directional derivatives exist and the derivative built from the directional derivatives is continuous. I think there is something that the definition does not match up with the one for Banach spaces, so it might be very hard to generalize beyond Banach spaces as the domain and keep a useful derivative.

[Moritz Doll]

But the thing that I would like to have is way more simple (and IMO way more relevant): I would like to say that a function is smooth from the reals (or non-negative reals) to Schwartz functions, to be able to state regularity of something like the propagator of the wave/Schrödinger equation (or heat) and having all of the calculus library for codomain being a TVS is the main obstacle.

[Sébastien Gouëzel]

Yury G. Kudryashov said:

I've recently found out about this approach to $C^k$. I don't know how exactly it relates to our definition in case of real normed spaces.

I was aware of this approach when I developed C^k in Mathlib. The book by Schikhof (Ultrametric calculus) is a very nice reference for that. It is a little bit alien to what we usually do on $\R$ or $\mathbb{C}$ because it is not written in terms of a sequence of iterated derivatives all of a similar nature. It turns out to be equivalent to the usual definition on $\R$ or $\mathbb{C}$, but the definitions and results are sufficiently different that it would be much harder to use in the usual situations. In fact, to me the main point of calculus, and the reason for its power, it that you can deduce properties of the function from properties of the derivative, and this doesn't really hold in this generalized context because there is no real notion of derivative. So, for practicality of use, I decided to go for a more classically-flavored definition.

If anyone has a use for the more exotic definition, I think it should be defined as a parallel hierarchy in Mathlib, not replacing the one we already have. But I don't know of applications beyond the theory itself, so I'm not sure there is a huge pressure or need for that in Mathlib.

[Kevin Buzzard]

I think that sometimes it is wise to bifurcate in the archimedean/nonarchimedean case even if it's strictly speaking possible to formalise everything in a universal way. For example, it's possible to define the adeles of $\mathbb{Q}$ as a restricted product of the completions of $\mathbb{Q}$, but we have an essentially completely disjoint API for archimedean and nonarchimedean completions, so in mathlib the adeles of a number field is defined as the product of (the restricted product of the nonarchimedean completions) and (the product of the archimedean completions) and we severely stress-tested this design decision in the FLT project throughout 2025 and I was very happy with it.

The first section of the fundamental book by Jacquet and Langlands (which we'll need for FLT) talks about Schwarz functions on a completion of a number field, so this is either $\R$ or $\mathbb{C}$ or a $p$-adic field, and I absolutely did not start screaming about $p$-adic fields when people started developing the classical theory of Schwarz functions, because even though I knew that in theory one could develop the theory in such a way that a small part of it applied to the $p$-adic case, in the $p$-adic case it's just locally constant functions with compact support, and I could see absolutely no point at all in arguing that the theory should apply in the $p$-adic case when it was simply far easier to just make the (far simpler) relevant definitions in the nonarchimedean case by hand.

There is an art to formalization -- you want your definitions to hold not in "the most generality" but in "the right generality". If we always went for the most generality then probably the bottom of our algebra hierarchy would be statements about objects of categories or something! We wouldn't have Zero and One, we'd have Element which unifies the two theories in a totally unhelpful way.

[Eric Wieser]

Eric Wieser said:

Done in #34348.

This should now be ready to go, which unblocks #34345 which generalizes Basic.lean to TVS. I had a quick go at generalizing Const.lean, but docs#hasFDerivWithinAt_singleton doesn't work without some thought

[Yury G. Kudryashov]

I will have some time tonight to review this and #34402 (unrelated)

[Yury G. Kudryashov]

Sent #34348 to bors. Please tell me when #34345 is ready for review.

[Eric Wieser]

@Yury G. Kudryashov, #34345 is ready

[Yury G. Kudryashov]

While thinking about generalizing more lemmas, I've found out that I don't know how to prove this lemma (and if it's true in a general TVS):

import Mathlib

open Asymptotics

theorem goal {α 𝕜 E : Type*} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
    [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
    {l : Filter α} {f g : α → E} (h : f =o[𝕜; l] g) :
    g =O[𝕜; l] (f + g) := by
  sorry

It's a part of IsEquivalentTVS.isThetaTVS, where IsEquivalentTVS is defined in the same way as docs#Asymptotics.IsEquivalent, but for TVS.

[Yury G. Kudryashov]

A version of this lemma docs#Asymptotics.IsLittleO.right_isBigO_add for normed spaces is used in the proof of docs#HasFDerivAtFilter.isBigO_sub_rev

[Anatole Dedecker]

I think this should at least be true in the locally convex settings, using the results of #34472

[Yury G. Kudryashov]

This is not something that we can require for any field K.

[Anatole Dedecker]

We can thanks to docs#PolynormableSpace, which encompasses all normed spaces

[Anatole Dedecker]

But it would be nicer to not have this assumption I agree

[Anatole Dedecker]

Wait actually I retract my claim: even in the locally convex it's not clear if it's true

[Anatole Dedecker]

Am I right that, in $\mathbb{R}^\mathbb{N}$ with the product topology, the function $f : \mathbb{N} \to \mathbb{R}^\mathbb{N}, n \mapsto (n^k)_k$ satisfies $f = o(f)$ at infinity? Because each coordinate is negligible compared to the next one. But then of course $f \neq O(f - f)$ so your lemma would be false?

[Yury G. Kudryashov]

Does it mean that our definition of f = o(g) in a TVS is bad?

[Anatole Dedecker]

I'm not sure to be honest. My guess (purely based on the locally convex/polynormable setting) is it's the only sensible thing, and it should give some interesting generalization (typically, we could upgrade docs#hasFDerivAt_pi to arbitrary products, which would allow stating things in a convenient way), but probably there's too many pathologies to generalize everything.

[Anatole Dedecker]

For anyone following along: in the locally convex setting, the criterion for $f = o(g)$ is: for any continuous seminorm $p$, there exists a continuous seminorm $q$ such that $p\circ f = o(q\circ g)$. The issue, IIUC, comes from this forall/exists asymmetry.

[Anatole Dedecker]

Aha, in fact this suggests a probably better behaved definition of asymptotic equivalents : for all continuous seminorm $p$, $p(f - g) = o(p(g))$ (and in general you replace the "forall seminorm" by "for any gauge of a neighborhood of zero").

I haven’t thought about the details though, so take this with a grain of salt.

[Yury G. Kudryashov]

This won't be helpful for derivatives, since we can't get it from f=o(g).

[Kevin Buzzard]

Is this generalisation for its own sake or are people really using little-o notation in the wild in situations where there isn't a canonical fixed norm?

[Yury G. Kudryashov]

People use derivatives without a canonical fixed norm. E.g.,

• derivative of a function $f\colon\mathbb R\to C^\infty(E, F)$;
• matrix spaces have no canonical norm in Mathlib.

[Yury G. Kudryashov]

For growth estimates, docs#Asymptotics.IsLittleO etc are more convenient, as they have more API. docs#Asymptotics.IsLittleOTVS was introduced to generalize the derivatives.

[Moritz Doll]

Sorry for being late to this discussion, but would it be easier if we restrict to the co-domain of $g$ being a normed space? then there is no seminorm $q$ to choose. For the derivatives that is all we need, right?

[Yury G. Kudryashov]

That's what we have now in docs#HasFDerivAt.isEquivalent_sub now.

[Yury G. Kudryashov]

UPD: sorry, I've misread what you were answering. I'll look into this later today.

[Moritz Doll]

What I would expect the definition for IsLittleOTVS to be is: $f = o(g)$ if for every continuous seminorm $p$, we have that $p(f) = o(\|g\|)$

[Yury G. Kudryashov]

I don't think that we should restrict this in the definition.

[Yury G. Kudryashov]

We have a definition that works for a function between two TVS, and it gives the right result for (semi)normed spaces. Why change it?

[Moritz Doll]

There is no need to change it, but maybe we want a characterisation in terms of the co-domain of f being polynormable and the co-domain of g being normable? And then it should be easy to prove the statement above. Or do you have a case where g maps into a locally convex space?