Equality of seminorm balls under a linear bijection preserves the seminorms

MathlibAnnex.SeminormBall.map_eq

theorem

Turns a ball-image equality into one seminorm inequality in each direction.

Statement

Let be real vector spaces with definite seminorms and , and write and . If a real-linear bijection satisfies , then

Assumptions

The spaces are real vector spaces. The seminorms satisfy and . The map is linear and bijective, and its image of the entire closed seminorm unit ball is exactly . No topology, continuity, measure, compactness, finite-dimensionality or volume equality is assumed.

Conclusion

The given map preserves the two seminorms pointwise. With ordinary norms this gives the separately stated norm-preservation result for a linear bijection carrying one closed unit ball onto the other.

Notes

The auxiliary forward inequality only needs definiteness of the domain seminorm and containment of ball images. In the equality theorem, definiteness of is used when that same inequality is applied to . The argument is algebraic.

Proof route

For , linearity and the seminorm axioms give equality. Suppose . Definiteness and nonnegativity give . The normalized vector satisfies , so . The forward ball containment gives . By linearity and seminorm homogeneity,

and multiplying by gives . This is the ball-containment lemma, valid for every after including zero. Since is bijective and , its inverse carries into . Apply the same lemma with to :

Together the two inequalities give the desired equality.

theorem map_eq
    [AddCommGroup E] [Module ℝ E]
    [AddCommGroup F] [Module ℝ F]
    (p : Seminorm ℝ E) (q : Seminorm ℝ F)
    (hp : ∀ x : E, p x = 0 → x = 0)
    (hq : ∀ y : F, q y = 0 → y = 0)
    (L : E →ₗ[ℝ] F) (hbij : Function.Bijective L)
    (hball : L '' p.closedBall 0 1 = q.closedBall 0 1) (x : E) :
    q (L x) = p x

noncomputable section

open Set MeasureTheory
open scoped ENNReal

namespace MathlibAnnex

namespace SeminormBall

variable {E F : Type*}

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project