Continuous linear maps bounded by a seminorm

MathlibAnnex.EquivalentSeminorm.IsContraction

def

Defines the pointwise contraction condition relative to a stored equivalent seminorm.

Statement

Let be real normed spaces and let be the seminorm of an equivalent-seminorm datum on , with stored constants satisfying for every and with continuous. A continuous real-linear map is a contraction relative to this datum exactly when for every .

Definition

For the given continuous linear map , define

Here is evaluated on the domain vector, and the norm is the codomain norm.

Assumptions

The map is already continuous and real-linear. The domain carries its reference norm and an equivalent-seminorm datum with positive comparison constants and continuity. The codomain is any real normed space, with the norm appearing on the left of the inequality. No dimension, completeness or bijectivity condition is imposed.

Conclusion

The declaration defines a proposition about the given map . The separately defined contraction set is precisely .

When a later application takes in the form of real functions on a finite index set, its default norm is the supremum norm. This is a specialization of the same predicate. The definition itself supplies neither an operator nor an inverse.

def IsContraction (A : E →L[ℝ] F) : Prop := ∀ x, ‖A x‖ ≤ M.p x

namespace EquivalentSeminorm

variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] (M : EquivalentSeminorm E)

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