The operator norm over ring scalars

Mathlib's operator norm ContinuousLinearMap.opNorm is the infimum of the uniform Lipschitz bounds {c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖}, but it is only available when the scalars form a nontrivially normed field. This file uses the same formula for continuous semilinear maps between seminormed modules over arbitrary semirings, as a scoped Norm instance in the scope TauCeti.RingOpNorm, and develops its basic theory.

Over an arbitrary normed ring a continuous linear map need not admit any uniform bound, and then the infimum is the junk value 0. The bound is guaranteed over Tate scalars, those whose norm admits a multiplicative pseudo-uniformiser ϖ (TauCeti.NormedRing.IsTate): exact scaling by the powers of ϖ moves every vector of nonzero norm into a fixed shell around the origin, where continuity at zero gives the estimate (TauCeti.NormedRing.IsTate.bound_of_continuous). Over Tate scalars the operator norm is therefore the least uniform bound, and the usual norm, triangle, ultrametric, composition and scalar laws follow.

Over a nontrivially normed field the scoped norm is definitionally Mathlib's operator norm (ContinuousLinearMap.ringOpNorm_eq_opNorm). The scope should not be opened over a field, where it would duplicate Mathlib's instance.

Main definitions

• ContinuousLinearMap.ringOpNorm: the infimum of the uniform bounds of a continuous semilinear map, installed as the scoped instance TauCeti.RingOpNorm.hasOpNorm.

Main results

• ContinuousLinearMap.isLeast_ringOpNorm: if a uniform bound exists, the operator norm is the least one.
• TauCeti.NormedRing.IsTate.bound_of_continuous: over Tate scalars every continuous linear map between seminormed modules with contractive scalar actions has a uniform bound.
• ContinuousLinearMap.le_ringOpNorm: ‖f x‖ ≤ ‖f‖ * ‖x‖ over Tate scalars.
• ContinuousLinearMap.ringOpNorm_le_of_ball, ContinuousLinearMap.ringOpNorm_le_of_nhds_zero: a linear bound near zero over Tate scalars bounds the operator norm.
• TauCeti.NormedRing.PseudoUniformizer.ringOpNorm_le_of_forall_norm_lt: a constant bound on a ball gives a quantitative global operator-norm bound by shell rescaling.
• LinearMap.norm_pi_apply_le_sum, LinearMap.norm_pi_apply_le_sup, ContinuousLinearMap.ringOpNorm_pi_eq_sup: finite-free coordinate bounds.
• ContinuousLinearMap.ringOpNorm_add_le, ContinuousLinearMap.ringOpNorm_add_le_max, ContinuousLinearMap.ringOpNorm_comp_le, ContinuousLinearMap.ringOpNorm_smul_le: the norm laws.
• ContinuousLinearMap.ringOpNorm_toSpanSingleton: right multiplication by v has norm ‖v‖ over a norm-one ring; in particular multiplication by a on a norm-one commutative ring has norm ‖a‖.

References

• C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.
• P. Schneider, Nonarchimedean Functional Analysis, Springer, 2002, §3.

The formula and API shape follow Mathlib's Mathlib/Analysis/Normed/Operator/Basic.lean; the ringOpNorm prefix distinguishes this scoped ring-scalar API from Mathlib's field-scalar API.

theorem TauCeti.NormedRing.PseudoUniformizer.bound_of_forall_norm_lt {R : Type u_1} {E : Type u_2} {F : Type u_3} {𝓕 : Type u_4} [SeminormedRing R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] [FunLike 𝓕 E F] [LinearMapClass 𝓕 R E F] (ϖ : PseudoUniformizer R) (f : 𝓕) {δ B : ℝ} (k : ℤ) (hδ : ‖↑ϖ.unit‖ ^ k < δ) (hf : ∀ (x : E), ‖x‖ < δ → ‖f x‖ ≤ B) (x : E) : ‖f x‖ ≤ B * (‖↑ϖ.unit‖ ^ (k + 1))⁻¹ * ‖x‖

A constant bound on a ball gives a global linear bound by rescaling with a multiplicative pseudo-uniformiser. Continuity of the linear map is not required.

theorem TauCeti.NormedRing.IsTate.bound_of_continuous {R : Type u_1} {E : Type u_2} {F : Type u_3} {𝓕 : Type u_4} [SeminormedRing R] [IsTate R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] [FunLike 𝓕 E F] [LinearMapClass 𝓕 R E F] (f : 𝓕) (hf : Continuous ⇑f) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : E), ‖f x‖ ≤ C * ‖x‖

Continuity implies a uniform bound over Tate scalars. A continuous linear map between seminormed modules with contractive scalar actions over a ring admitting a multiplicative pseudo-uniformiser satisfies ‖f x‖ ≤ C * ‖x‖ for some C > 0.

noncomputable def ContinuousLinearMap.ringOpNorm {R : Type u_1} {S : Type u_2} {E : Type u_4} {F : Type u_5} [Semiring R] [Semiring S] {σ : R →+* S} [SeminormedAddCommGroup E] [Module R E] [SeminormedAddCommGroup F] [Module S F] (f : E →SL[σ] F) : ℝ

The operator norm of a continuous semilinear map between seminormed modules over semirings: the infimum of its uniform bounds. It is the formula of Mathlib's ContinuousLinearMap.opNorm without the assumption that the scalars form a field.

@[instance_reducible]

noncomputable def TauCeti.RingOpNorm.hasOpNorm {R : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_4} [Semiring R] [Semiring S] {σ : R →+* S} [SeminormedAddCommGroup E] [Module R E] [SeminormedAddCommGroup F] [Module S F] : Norm (E →SL[σ] F)

The operator norm over ring scalars, as a scoped instance.

theorem ContinuousLinearMap.ringOpNorm_def {R : Type u_1} {S : Type u_2} {E : Type u_4} {F : Type u_5} [Semiring R] [Semiring S] {σ : R →+* S} [SeminormedAddCommGroup E] [Module R E] [SeminormedAddCommGroup F] [Module S F] (f : E →SL[σ] F) : ‖f‖ = sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}

The operator norm is the infimum of the nonnegative uniform bounds.

theorem ContinuousLinearMap.ringOpNorm_bounds_bddBelow {R : Type u_1} {S : Type u_2} {E : Type u_4} {F : Type u_5} [Semiring R] [Semiring S] {σ : R →+* S} [SeminormedAddCommGroup E] [Module R E] [SeminormedAddCommGroup F] [Module S F] {f : E →SL[σ] F} : BddBelow {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}

The set of nonnegative uniform bounds is bounded below.

theorem ContinuousLinearMap.ringOpNorm_nonneg {R : Type u_1} {S : Type u_2} {E : Type u_4} {F : Type u_5} [Semiring R] [Semiring S] {σ : R →+* S} [SeminormedAddCommGroup E] [Module R E] [SeminormedAddCommGroup F] [Module S F] (f : E →SL[σ] F) : 0 ≤ ‖f‖

The operator norm is nonnegative.

theorem ContinuousLinearMap.ringOpNorm_le_bound {R : Type u_1} {S : Type u_2} {E : Type u_4} {F : Type u_5} [Semiring R] [Semiring S] {σ : R →+* S} [SeminormedAddCommGroup E] [Module R E] [SeminormedAddCommGroup F] [Module S F] (f : E →SL[σ] F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ M

If one controls the norm of every f x, then one controls the norm of f.

theorem ContinuousLinearMap.isLeast_ringOpNorm {R : Type u_1} {S : Type u_2} {E : Type u_4} {F : Type u_5} [Semiring R] [Semiring S] {σ : R →+* S} [SeminormedAddCommGroup E] [Module R E] [SeminormedAddCommGroup F] [Module S F] (f : E →SL[σ] F) (h : ∃ (C : ℝ), ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : IsLeast {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} ‖f‖

The bound at the infimum: if f has some uniform bound, then its operator norm is its least nonnegative uniform bound.

theorem ContinuousLinearMap.le_ringOpNorm_of_exists_bound {R : Type u_1} {S : Type u_2} {E : Type u_4} {F : Type u_5} [Semiring R] [Semiring S] {σ : R →+* S} [SeminormedAddCommGroup E] [Module R E] [SeminormedAddCommGroup F] [Module S F] (f : E →SL[σ] F) (h : ∃ (C : ℝ), ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) (x : E) : ‖f x‖ ≤ ‖f‖ * ‖x‖

If f has some uniform bound, then ‖f x‖ ≤ ‖f‖ * ‖x‖.

theorem ContinuousLinearMap.ringOpNorm_eq_of_bounds {R : Type u_1} {S : Type u_2} {E : Type u_4} {F : Type u_5} [Semiring R] [Semiring S] {σ : R →+* S} [SeminormedAddCommGroup E] [Module R E] [SeminormedAddCommGroup F] [Module S F] {f : E →SL[σ] F} {M : ℝ} (hM₀ : 0 ≤ M) (h_above : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖) (h_below : ∀ N ≥ 0, (∀ (x : E), ‖f x‖ ≤ N * ‖x‖) → M ≤ N) : ‖f‖ = M

A nonnegative uniform bound below every other one is the operator norm.

@[simp]

theorem ContinuousLinearMap.ringOpNorm_zero {R : Type u_1} {S : Type u_2} {E : Type u_4} {F : Type u_5} [Semiring R] [Semiring S] {σ : R →+* S} [SeminormedAddCommGroup E] [Module R E] [SeminormedAddCommGroup F] [Module S F] : ‖0‖ = 0

The norm of the 0 operator is 0.

theorem ContinuousLinearMap.ringOpNorm_id_le {R : Type u_1} {E : Type u_4} [Semiring R] [SeminormedAddCommGroup E] [Module R E] : ‖ContinuousLinearMap.id R E‖ ≤ 1

The norm of the identity is at most 1.

@[simp]

theorem ContinuousLinearMap.ringOpNorm_id {R : Type u_1} {E : Type u_4} [Semiring R] [SeminormedAddCommGroup E] [Module R E] [NontrivialTopology E] : ‖ContinuousLinearMap.id R E‖ = 1

If some vector has nonzero norm, then the identity has norm 1.

theorem ContinuousLinearMap.ringOpNorm_comp_le_of_exists_bound {R : Type u_1} {S : Type u_2} {T : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [Semiring R] [Semiring S] [Semiring T] {σ : R →+* S} {τ : S →+* T} {ρ : R →+* T} [RingHomCompTriple σ τ ρ] [SeminormedAddCommGroup E] [Module R E] [SeminormedAddCommGroup F] [Module S F] [SeminormedAddCommGroup G] [Module T G] (g : F →SL[τ] G) (f : E →SL[σ] F) (hg : ∃ (C : ℝ), ∀ (y : F), ‖g y‖ ≤ C * ‖y‖) (hf : ∃ (C : ℝ), ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : ‖g ∘SL f‖ ≤ ‖g‖ * ‖f‖

A composition of maps with uniform bounds is bounded by the product of their operator norms.

theorem ContinuousLinearMap.ringOpNorm_le_of_ball {R : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (f : E →L[R] F) {ε C : ℝ} (hε : 0 < ε) (hC : 0 ≤ C) (hf : ∀ x ∈ Metric.ball 0 ε, ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C

Over a Tate ring, a linear norm bound ‖f x‖ ≤ C * ‖x‖ on a ball around 0 extends to all of E and bounds the operator norm ‖f‖ by C.

theorem ContinuousLinearMap.ringOpNorm_le_of_nhds_zero {R : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (f : E →L[R] F) {C : ℝ} (hC : 0 ≤ C) (hf : ∀ᶠ (x : E) in nhds 0, ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C

Over a Tate ring, if ‖f x‖ ≤ C * ‖x‖ holds in a neighbourhood of 0, then ‖f‖ ≤ C.

theorem TauCeti.NormedRing.PseudoUniformizer.ringOpNorm_le_of_forall_norm_lt {R : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedRing R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (ϖ : PseudoUniformizer R) (f : E →L[R] F) {δ B : ℝ} (k : ℤ) (hδ : ‖↑ϖ.unit‖ ^ k < δ) (hf : ∀ (x : E), ‖x‖ < δ → ‖f x‖ ≤ B) : ‖f‖ ≤ B * (‖↑ϖ.unit‖ ^ (k + 1))⁻¹

Quantitative local-to-global operator-norm bound. If ϖ is a multiplicative pseudo-uniformiser on R, ‖(ϖ.unit : R)‖ ^ k < δ, and ‖f x‖ ≤ B for every x of norm < δ, then ‖f‖ ≤ B * (‖(ϖ.unit : R)‖ ^ (k + 1))⁻¹.

@[simp]

theorem ContinuousLinearMap.ringOpNorm_neg {R : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [Ring S] {σ : R →+* S} [SeminormedAddCommGroup E] [Module R E] [SeminormedAddCommGroup F] [Module S F] (f : E →SL[σ] F) : ‖-f‖ = ‖f‖

The operator norm is invariant under negation.

theorem ContinuousLinearMap.ringOpNorm_bound {R : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (f : E →L[R] F) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : E), ‖f x‖ ≤ C * ‖x‖

Over Tate scalars every continuous linear map has a uniform bound.

theorem ContinuousLinearMap.le_ringOpNorm {R : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (f : E →L[R] F) (x : E) : ‖f x‖ ≤ ‖f‖ * ‖x‖

The fundamental property of the operator norm over Tate scalars: ‖f x‖ ≤ ‖f‖ * ‖x‖.

theorem ContinuousLinearMap.le_of_ringOpNorm_le {R : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (f : E →L[R] F) {c : ℝ} (h : ‖f‖ ≤ c) (x : E) : ‖f x‖ ≤ c * ‖x‖

A bound on the operator norm bounds every value.

theorem ContinuousLinearMap.ringOpNorm_le_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] {f : E →L[R] F} {M : ℝ} (hMp : 0 ≤ M) : ‖f‖ ≤ M ↔ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖

Over Tate scalars, ‖f‖ ≤ M exactly when M is a uniform bound for f.

theorem ContinuousLinearMap.ratio_le_ringOpNorm {R : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (f : E →L[R] F) (x : E) : ‖f x‖ / ‖x‖ ≤ ‖f‖

The operator norm is an upper bound for the ratios ‖f x‖ / ‖x‖.

theorem ContinuousLinearMap.ringOpNorm_add_le {R : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (f g : E →L[R] F) : ‖f + g‖ ≤ ‖f‖ + ‖g‖

The operator norm satisfies the triangle inequality.

theorem ContinuousLinearMap.ringOpNorm_add_le_max {R : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] [IsUltrametricDist F] (f g : E →L[R] F) : ‖f + g‖ ≤ max ‖f‖ ‖g‖

The operator norm is ultrametric when the target is.

theorem ContinuousLinearMap.ringOpNorm_comp_le {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] [SeminormedAddCommGroup G] [Module R G] [IsBoundedSMul R G] (g : F →L[R] G) (f : E →L[R] F) : ‖g ∘SL f‖ ≤ ‖g‖ * ‖f‖

The operator norm is submultiplicative.

theorem ContinuousLinearMap.ringOpNorm_smul_le {R : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] {S : Type u_5} [SeminormedAddCommGroup S] [DistribSMul S F] [IsBoundedSMul S F] [SMulCommClass R S F] (c : S) (f : E →L[R] F) : ‖c • f‖ ≤ ‖c‖ * ‖f‖

Scalar multiplication of operators is contractive for the operator norm.

@[simp]

theorem ContinuousLinearMap.ringOpNorm_toSpanSingleton {R : Type u_1} {E : Type u_2} [SeminormedRing R] [NormOneClass R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] (v : E) : ‖toSpanSingleton R v‖ = ‖v‖

Right multiplication by v has norm ‖v‖ over a norm-one ring: the map a ↦ a • v from R to E. For E = R commutative, this is multiplication by v.

theorem ContinuousLinearMap.ringOpNorm_eq_opNorm {K : Type u_1} {L : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField K] [NontriviallyNormedField L] {σ : K →+* L} [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace L F] (f : E →SL[σ] F) : f.ringOpNorm = f.opNorm

Over a nontrivially normed field, the operator norm over ring scalars is Mathlib's operator norm ContinuousLinearMap.opNorm.

Finite-free operator bounds

theorem LinearMap.norm_pi_apply_le_sum {R : Type u_1} {N : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [SeminormedRing R] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] (f : (ι → R) →ₗ[R] N) (x : ι → R) : ‖f x‖ ≤ (∑ i : ι, ‖f (Pi.single i 1)‖) * ‖x‖

Any linear map f : (ι → R) →ₗ[R] N on a finite product satisfies the coordinate bound ‖f x‖ ≤ (∑ i, ‖f (Pi.single i 1)‖) * ‖x‖.

theorem LinearMap.norm_pi_apply_le_sup {R : Type u_1} {N : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [SeminormedRing R] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] [IsUltrametricDist N] (f : (ι → R) →ₗ[R] N) (x : ι → R) : ‖f x‖ ≤ ↑(Finset.univ.sup fun (i : ι) => ‖f (Pi.single i 1)‖₊) * ‖x‖

When the target module N is ultrametric, any linear map f : (ι → R) →ₗ[R] N on a finite product is bounded by the supremum of the norms of the images of the standard basis vectors: ‖f x‖ ≤ (Finset.univ.sup fun i ↦ ‖f (Pi.single i 1)‖₊) * ‖x‖.

theorem ContinuousLinearMap.ringOpNorm_pi_le_sup {R : Type u_1} {N : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [SeminormedRing R] [SeminormedAddCommGroup N] [IsUltrametricDist N] [Module R N] [IsBoundedSMul R N] (f : (ι → R) →L[R] N) : ‖f‖ ≤ ↑(Finset.univ.sup fun (i : ι) => ‖f (Pi.single i 1)‖₊)

The operator norm of f : (ι → R) →L[R] N into an ultrametric module is bounded by the supremum of the norms of the images of the standard basis vectors.

theorem ContinuousLinearMap.ringOpNorm_pi_eq_sup {R : Type u_1} {N : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [SeminormedRing R] [SeminormedAddCommGroup N] [IsUltrametricDist N] [Module R N] [IsBoundedSMul R N] [TauCeti.NormedRing.IsTate R] (f : (ι → R) →L[R] N) : ‖f‖ = ↑(Finset.univ.sup fun (i : ι) => ‖f (Pi.single i 1)‖₊)

Over a Tate ring, the operator norm of f : (ι → R) →L[R] N into an ultrametric module is the supremum of the norms of the images of the standard basis vectors Pi.single i 1.