Antilipschitz for linear maps

Stream: maths

[Yury G. Kudryashov]

Currently, different lemmas use different spelling for the assumption "a CLM f' is an expanding map":

• docs#HasFDerivAtFilter.isBigO_sub_rev uses {C} (h : AntilipschitzWith C f');
• docs#HasStrictFDerivAt.isBigO_sub_rev assumes that f' is an equivalence (which is stronger than what we actually need);
• docs#HasFDerivWithinAt.eventually_ne assumes ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖

I think that we should normalize these assumptions, preferrably to something that doesn't depend on the norm, so that we can generalize to TVS later.

[Yury G. Kudryashov]

/poll Possible options:
id =O[⊤] f', then generalize to TVS using not-yet-in-mathlib IsBigOTVS;
id =O[𝓝 0] f', then generalize to TVS using not-yet-in-mathlib IsBigOTVS;
comap f (𝓝 0) ≤ 𝓝 0
new definition with constructors/lemmas linking to all other versions here.

[Yury G. Kudryashov]

For the comap version see docs#LinearMap.antilipschitz_of_comap_nhds_le

[Yury G. Kudryashov]

The main issues with the first 2 approaches are:

• it isn't clear which one is better;
• we'll have to either redo Is*OTVS for different scalar fields on the LHS and RHS, or restrict this normal form to linear, not semilinear maps.

[Yury G. Kudryashov]

Given that we have many different options, I slightly prefer to add a new definition here.

[Eric Wieser]

I have repeatedly hallucinated the existence of Lipschitz and Antilipschitz as existentially-quantified version of the With versions, so I would be in favor of them being introduced one way or another

[Yury G. Kudryashov]

We may need something LinearMap-specific too, because we can't say Antilipschitz without having a metric, and I want to use this as an assumption in some theorems about derivatives.

[Yury G. Kudryashov]

Currently, these lemmas use normed spaces, but we're going to generalize them to TVS soon.

[Antoine Chambert-Loir]

Isn't it strictness of the linear map? (Quotient topology coincides with the subspace topology on the range)?

[Yury G. Kudryashov]

Why quotient topology? This condition implies injectivity (at least, for Hausdorff spaces).

[Yury G. Kudryashov]

It may be equivalent to IsOpenEmbedding (for continuous linear maps), but I'm too sleepy now to be sure.

[Anatole Dedecker]

Yes, nhds 0 = comap f (nhds zero) is precisely the same as IsOpenEmbedding as long as f is an add group morphism between topological additive groups. This even holds under the condition that addition of any fixed constant is continuous, but there’s no hope for any of this to hold in monoids (I don’t think we care though: in any more general setup, I claim that docs#IsOpenEmbedding is obviously the right analog)

[Antoine Chambert-Loir]

Sorry, you're right.