Operator norm on non-continuous linear map

Stream: Is there code for X?

[Gregory Wickham]

Is there code that defines the operator norm on a non-continuous linear map and to construct a continuous linear map from a linear map and a proof that its operator norm is finite?

[Aaron Liu]

found docs#LinearMap.mkContinuous

[Niels Voss]

If your vector spaces are finite dimensional you can use docs#LinearMap.toContinuousLinearMap

[Aaron Liu]

that seems like a bad name for a few reasons

[Niels Voss]

What are those reasons? Is it because it doesn't mention finite-dimensionality?

[Aaron Liu]

here's a reason

import Mathlib

variable {R E F : Type*} [Semiring R]
    [SeminormedAddCommGroup E] [Module R E]
    [SeminormedAddCommGroup F] [Module R F]
    (f : E ≃ₗᵢ[R] F) -- `R`-linear isometry equiv

/-
Application type mismatch: The argument
  ↑f.toLinearEquiv
has type
  E →ₛₗ[@RingHom.id R (@Semiring.toNonAssocSemiring R inst✝⁴)] F
but is expected to have type
  ?m.47 →ₛₗ[@RingHom.id ?m.45 (@Semiring.toNonAssocSemiring ?m.45 Field.toSemifield.toDivisionSemiring.toSemiring)]
    ?m.53
in the application
  LinearMap.toContinuousLinearMap ↑f.toLinearEquiv
-/
#check f.toContinuousLinearMap

[Aaron Liu]

things named toFoo should be forgetful

[Aaron Liu]

if you want to upgrade it should be called ofBar

[Aaron Liu]

also I never would've guessed from the name that it's a 𝕜-linear equivalence