A strict lower bound on a norm’s unit sphere

MathlibAnnex.FiniteSup.FinMapAlmostIsometric

definition

Defines the strict lower condition on a fixed norm unit sphere.

Statement

Let be arbitrary, including zero. Use reference coordinates with the sup norm and standard basis. The supplied continuous seminorm has constants satisfying Thus is a norm; it can differ from the reference sup norm. Fix any and continuous real linear , with the target sup norm. Define the property by

Definition

The property requires the displayed strict lower bound at every -unit vector. It is a condition on the given map , not a construction of a new map.

Assumptions

The inputs are the continuous seminorm with its positive two-sided comparison bounds, any real , and the fixed continuous real linear map . Neither an upper estimate on , positivity of , nor injectivity of is an input to this definition.

Conclusion

This is only the lower unit-sphere condition. In dimension zero the unit sphere is empty and the condition is vacuous.

As a separate consequence, let . Positive definiteness gives , and Apply the condition at that same vector and multiply by to obtain This is the lower bound away from zero. It adds no upper estimate.

def FinMapAlmostIsometric {n N : ℕ} (M : NormModel n) (ε : ℝ)
    (A : Coord n →L[ℝ] SupCoord N) : Prop :=
  ∀ x : Coord n, M.p x = 1 → 1 - ε < ‖A x‖

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