continuous_linear_equiv

Stream: Is there code for X?

[Frédéric Dupuis]

Is there a good way to define a continuous_linear_equiv (where by "good" I mean via a bound rather than by proving continuity directly)? Basically I'm looking for something similar to linear_map.mk_continuous.

[Heather Macbeth]

Do you have bounds in both directions? Or are you planning to use the Banach open mapping theorem?

[Frédéric Dupuis]

Let's say I have bounds in both directions -- are you aware of any lemmas I could use?

[Yury G. Kudryashov]

(deleted)

[Heather Macbeth]

There is docs#continuous_linear_equiv.equiv_of_inverse, to make a continuous linear equiv from two continuous linear maps.

[Heather Macbeth]

And then, as you said, there is docs#linear_map.mk_continuous to make each of the directions a continuous linear map, from the bounds.

[Heather Macbeth]

Would this work in your situation?

[Yury G. Kudryashov]

Probably you should wrap it into linear_equiv.to_continuous_linear_equiv_of_bounds.

[Yury G. Kudryashov]

And add this def to topology/algebra/module.

[Heather Macbeth]

Alternatively, if you have an existing linear equiv, by definition (docs#continuous_linear_equiv), it becomes a continuous linear equiv by checking that both directions are continuous. And you can use docs#linear_map.continuous_of_bound for this.

[Frédéric Dupuis]

Thanks! I was hoping for a way that involves fewer hoops to jump through, but I'll just code it as Yury suggests.

[Yury G. Kudryashov]

Heather explained two ways to write linear_equiv.to_continuous_linear_equiv.

[Frédéric Dupuis]

Yes -- or if anything these are two functions we would want to have!

[Frédéric Dupuis]

Also, I know you suggested putting them in topology/algebra/module, but wouldn't analysis/normed_space/operator_norm (alongside linear_map.mk_continuous) be a better place, given that there are norms involved?

[Frédéric Dupuis]

#4583