Scalar actions and pointwise norms on C₀(α, β)

Mathlib equips the space C₀(α, β) of continuous functions vanishing at infinity with the sup distance and, for normed fields, with a normed-space structure. This file supplies the structure needed for scalar actions beyond normed fields:

• ZeroAtInftyContinuousMap.instIsBoundedSMul: a bounded scalar action on β induces one on C₀(α, β), so for instance C₀(α, R) is a module with contractive action over a seminormed ring R;
• ZeroAtInftyContinuousMap.instContinuousConstSMul: a continuous distributive scalar action on an additive uniform group β induces continuous fixed-scalar multiplication on C₀(α, β);
• ZeroAtInftyContinuousMap.norm_le and ZeroAtInftyContinuousMap.norm_eq_iSup_norm: the norm on C₀(α, β) is the supremum of the pointwise norms;
• ZeroAtInftyContinuousMap.evalCLM: evaluation at a point as a continuous linear map over an arbitrary semiring of scalars;
• ZeroAtInftyContinuousMap.compLeft: a continuous linear map u : E →L[R] F with a uniform bound ‖u x‖ ≤ C * ‖x‖ acts pointwise as a continuous linear map C₀(α, E) →L[R] C₀(α, F);
• ZeroAtInftyContinuousMap.congrLeft: a homeomorphism α ≃ₜ β induces a linear isometry equivalence C₀(α, E) ≃ₗᵢ[R] C₀(β, E).

With α discrete these are the basic structures of the model space C₀(I, R) of nonarchimedean functional analysis over normed rings; its coordinate structure is developed in TauCeti.Topology.ContinuousMap.ZeroAtInfty.Discrete.

instance ZeroAtInftyContinuousMap.instIsBoundedSMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] {𝕜 : Type u_3} [PseudoMetricSpace 𝕜] [Zero 𝕜] [SMulZeroClass 𝕜 β] [IsBoundedSMul 𝕜 β] : IsBoundedSMul 𝕜 (ZeroAtInftyContinuousMap α β)

A bounded scalar action on β induces a bounded scalar action on C₀(α, β). In particular C₀(α, R) has a contractive scalar action of a seminormed ring R.

@[instance 90]

instance ZeroAtInftyContinuousMap.instContinuousConstSMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PseudoMetricSpace β] [AddGroup β] [IsUniformAddGroup β] {R : Type u_3} [DistribSMul R β] [ContinuousConstSMul R β] : ContinuousConstSMul R (ZeroAtInftyContinuousMap α β)

A continuous distributive scalar action on an additive uniform group induces continuous fixed-scalar multiplication on functions vanishing at infinity, with their sup metric.

@[simp]

theorem ZeroAtInftyContinuousMap.coe_sum {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {ι : Type u_3} (s : Finset ι) (f : ι → ZeroAtInftyContinuousMap α β) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

The coercion to functions commutes with finite sums.

theorem ZeroAtInftyContinuousMap.norm_coe_le_norm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : ZeroAtInftyContinuousMap α β) (x : α) : ‖f x‖ ≤ ‖f‖

The norm of a function vanishing at infinity bounds the norm of each of its values.

theorem ZeroAtInftyContinuousMap.norm_le {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [SeminormedAddCommGroup β] {f : ZeroAtInftyContinuousMap α β} {C : ℝ} (hC : 0 ≤ C) : ‖f‖ ≤ C ↔ ∀ (x : α), ‖f x‖ ≤ C

The norm of a function vanishing at infinity is bounded by C ≥ 0 exactly when each of its values is.

theorem ZeroAtInftyContinuousMap.norm_eq_iSup_norm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : ZeroAtInftyContinuousMap α β) : ‖f‖ = ⨆ (x : α), ‖f x‖

The norm of a function vanishing at infinity is the supremum of the norms of its values.

def ZeroAtInftyContinuousMap.evalCLM {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [SeminormedAddCommGroup β] (𝕜 : Type u_3) [Semiring 𝕜] [Module 𝕜 β] [ContinuousConstSMul 𝕜 β] (x : α) : ZeroAtInftyContinuousMap α β →L[𝕜] β

Evaluation at a point, as a continuous linear map C₀(α, β) →L[𝕜] β.

@[simp]

theorem ZeroAtInftyContinuousMap.evalCLM_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [SeminormedAddCommGroup β] (𝕜 : Type u_3) [Semiring 𝕜] [Module 𝕜 β] [ContinuousConstSMul 𝕜 β] (x : α) (f : ZeroAtInftyContinuousMap α β) : (evalCLM 𝕜 x) f = f x

evalCLM 𝕜 x evaluates at x.

@[simp]

theorem ZeroAtInftyContinuousMap.norm_comp_toCocompactMap {α : Type u_1} [TopologicalSpace α] {β : Type u_3} {E : Type u_5} [TopologicalSpace β] [SeminormedAddCommGroup E] (f : ZeroAtInftyContinuousMap β E) (e : α ≃ₜ β) : ‖f.comp e.toCocompactMap‖ = ‖f‖

Precomposition with a homeomorphism preserves the norm of a function vanishing at infinity.

def ZeroAtInftyContinuousMap.compLeft {α : Type u_1} [TopologicalSpace α] {R : Type u_4} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [SeminormedAddCommGroup F] [Module R F] [ContinuousConstSMul R F] (u : E →L[R] F) (hu : ∃ (C : ℝ), ∀ (x : E), ‖u x‖ ≤ C * ‖x‖) : ZeroAtInftyContinuousMap α E →L[R] ZeroAtInftyContinuousMap α F

Pointwise action of a bounded coefficient map. A continuous linear map u : E →L[R] F with a uniform bound ‖u x‖ ≤ C * ‖x‖ acts on C₀(α, E) by postcomposition, giving a continuous linear map C₀(α, E) →L[R] C₀(α, F).

@[simp]

theorem ZeroAtInftyContinuousMap.compLeft_apply {α : Type u_1} [TopologicalSpace α] {R : Type u_4} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [SeminormedAddCommGroup F] [Module R F] [ContinuousConstSMul R F] (u : E →L[R] F) (hu : ∃ (C : ℝ), ∀ (x : E), ‖u x‖ ≤ C * ‖x‖) (f : ZeroAtInftyContinuousMap α E) (x : α) : ((compLeft u hu) f) x = u (f x)

compLeft u hu applies u pointwise.

theorem ZeroAtInftyContinuousMap.compLeft_comp {α : Type u_1} [TopologicalSpace α] {R : Type u_4} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [SeminormedAddCommGroup F] [Module R F] [ContinuousConstSMul R F] {G : Type u_7} [SeminormedAddCommGroup G] [Module R G] [ContinuousConstSMul R G] (v : F →L[R] G) (u : E →L[R] F) (hv : ∃ (C : ℝ), ∀ (y : F), ‖v y‖ ≤ C * ‖y‖) (hu : ∃ (C : ℝ), ∀ (x : E), ‖u x‖ ≤ C * ‖x‖) (hvu : ∃ (C : ℝ), ∀ (x : E), ‖(v ∘SL u) x‖ ≤ C * ‖x‖) : compLeft (v ∘SL u) hvu = compLeft v hv ∘SL compLeft u hu

The coordinatewise action of a composite is the composite of the coordinatewise actions.

theorem ZeroAtInftyContinuousMap.norm_compLeft_apply_le {α : Type u_1} [TopologicalSpace α] {R : Type u_4} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [SeminormedAddCommGroup F] [Module R F] [ContinuousConstSMul R F] (u : E →L[R] F) {C : ℝ} (hC : ∀ (x : E), ‖u x‖ ≤ C * ‖x‖) (f : ZeroAtInftyContinuousMap α E) : ‖(compLeft u ⋯) f‖ ≤ C * ‖f‖

A uniform bound C for u is also a uniform bound for its coordinatewise action.

theorem ZeroAtInftyContinuousMap.exists_norm_compLeft_apply_le {α : Type u_1} [TopologicalSpace α] {R : Type u_4} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [SeminormedAddCommGroup F] [Module R F] [ContinuousConstSMul R F] (u : E →L[R] F) (hu : ∃ (C : ℝ), ∀ (x : E), ‖u x‖ ≤ C * ‖x‖) : ∃ (C : ℝ), ∀ (f : ZeroAtInftyContinuousMap α E), ‖(compLeft u hu) f‖ ≤ C * ‖f‖

The coordinatewise action of a bounded coefficient map is itself uniformly bounded.

def ZeroAtInftyContinuousMap.congrLeft {α : Type u_1} [TopologicalSpace α] {β : Type u_3} (R : Type u_4) (E : Type u_5) [TopologicalSpace β] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] (e : α ≃ₜ β) : ZeroAtInftyContinuousMap α E ≃ₗᵢ[R] ZeroAtInftyContinuousMap β E

Reindexing along a homeomorphism. A homeomorphism e : α ≃ₜ β identifies C₀(α, E) with C₀(β, E) isometrically, by f ↦ f ∘ e.symm. For discrete index types, any equivalence e gives such a homeomorphism e.toHomeomorphOfDiscrete.

@[simp]

theorem ZeroAtInftyContinuousMap.congrLeft_apply {α : Type u_1} [TopologicalSpace α] {β : Type u_3} {R : Type u_4} {E : Type u_5} [TopologicalSpace β] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] (e : α ≃ₜ β) (f : ZeroAtInftyContinuousMap α E) (y : β) : ((congrLeft R E e) f) y = f (e.symm y)

congrLeft R E e f is f ∘ e.symm.

@[simp]

theorem ZeroAtInftyContinuousMap.congrLeft_symm {α : Type u_1} [TopologicalSpace α] {β : Type u_3} {R : Type u_4} {E : Type u_5} [TopologicalSpace β] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] (e : α ≃ₜ β) : (congrLeft R E e).symm = congrLeft R E e.symm

The inverse of reindexing along e is reindexing along e.symm.

@[simp]

theorem ZeroAtInftyContinuousMap.congrLeft_refl {α : Type u_1} [TopologicalSpace α] {R : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] : congrLeft R E (Homeomorph.refl α) = LinearIsometryEquiv.refl R (ZeroAtInftyContinuousMap α E)

Reindexing along the identity is the identity.

theorem ZeroAtInftyContinuousMap.congrLeft_trans {α : Type u_1} [TopologicalSpace α] {β : Type u_3} {R : Type u_4} {E : Type u_5} [TopologicalSpace β] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] {γ : Type u_7} [TopologicalSpace γ] (e : α ≃ₜ β) (e' : β ≃ₜ γ) : congrLeft R E (e.trans e') = (congrLeft R E e).trans (congrLeft R E e')

Reindexing along a composite is the composite of the reindexings.

theorem ZeroAtInftyContinuousMap.congrLeft_compLeft {α : Type u_1} [TopologicalSpace α] {β : Type u_3} {R : Type u_4} {E : Type u_5} {F : Type u_6} [TopologicalSpace β] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [SeminormedAddCommGroup F] [Module R F] [ContinuousConstSMul R F] (e : α ≃ₜ β) (u : E →L[R] F) (hu : ∃ (C : ℝ), ∀ (x : E), ‖u x‖ ≤ C * ‖x‖) (f : ZeroAtInftyContinuousMap α E) : (congrLeft R F e) ((compLeft u hu) f) = (compLeft u hu) ((congrLeft R E e) f)

Reindexing commutes with the coordinatewise action of a bounded coefficient map.