Norm on the continuous affine maps between normed vector spaces.

We define a norm on the space of continuous affine maps between normed vector spaces by defining the norm of f : V →ᴬ[𝕜] W to be ‖f‖ = max ‖f 0‖ ‖f.cont_linear‖. This is chosen so that we have a linear isometry: (V →ᴬ[𝕜] W) ≃ₗᵢ[𝕜] W × (V →L[𝕜] W).

The abstract picture is that for an affine space P modelled on a vector space V, together with a vector space W, there is an exact sequence of 𝕜-modules: 0 → C → A → L → 0 where C, A are the spaces of constant and affine maps P → W and L is the space of linear maps V → W.

Any choice of a base point in P corresponds to a splitting of this sequence so in particular if we take P = V, using 0 : V as the base point provides a splitting, and we prove this is an isometric decomposition.

On the other hand, choosing a base point breaks the affine invariance so the norm fails to be submultiplicative: for a composition of maps, we have only ‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖.

Main definitions:

• ContinuousAffineMap.hasNorm
• ContinuousAffineMap.norm_comp_le
• ContinuousAffineMap.toConstProdContinuousLinearMap

noncomputable instance ContinuousAffineMap.hasNorm {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedAddCommGroup W] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] : Norm (V →ᴬ[𝕜] W)

Note that unlike the operator norm for linear maps, this norm is not submultiplicative: we do not necessarily have ‖f.comp g‖ ≤ ‖f‖ * ‖g‖. See norm_comp_le for what we can say.

Equations

• ContinuousAffineMap.hasNorm = { norm := fun (f : V →ᴬ[𝕜] W) => max ‖f 0‖ ‖f.contLinear‖ }

theorem ContinuousAffineMap.norm_def {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedAddCommGroup W] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] (f : V →ᴬ[𝕜] W) : ‖f‖ = max ‖f 0‖ ‖f.contLinear‖

theorem ContinuousAffineMap.norm_contLinear_le {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedAddCommGroup W] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] (f : V →ᴬ[𝕜] W) : ‖f.contLinear‖ ≤ ‖f‖

theorem ContinuousAffineMap.norm_image_zero_le {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedAddCommGroup W] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] (f : V →ᴬ[𝕜] W) : ‖f 0‖ ≤ ‖f‖

@[simp]

theorem ContinuousAffineMap.norm_eq {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedAddCommGroup W] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] (f : V →ᴬ[𝕜] W) (h : f 0 = 0) : ‖f‖ = ‖f.contLinear‖

noncomputable instance ContinuousAffineMap.instNormedAddCommGroup {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedAddCommGroup W] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] : NormedAddCommGroup (V →ᴬ[𝕜] W)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance ContinuousAffineMap.instNormedSpace {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedAddCommGroup W] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] : NormedSpace 𝕜 (V →ᴬ[𝕜] W)

Equations

• ContinuousAffineMap.instNormedSpace = { toModule := ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul, norm_smul_le := ⋯ }

theorem ContinuousAffineMap.norm_comp_le {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} [NormedAddCommGroup V] [NormedAddCommGroup W] [NormedAddCommGroup W₂] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] [NormedSpace 𝕜 W₂] (f : V →ᴬ[𝕜] W) (g : W₂ →ᴬ[𝕜] V) : ‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

noncomputable def ContinuousAffineMap.toConstProdContinuousLinearMap (𝕜 : Type u_1) (V : Type u_2) (W : Type u_3) [NormedAddCommGroup V] [NormedAddCommGroup W] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] : (V →ᴬ[𝕜] W) ≃ₗᵢ[𝕜] W × (V →L[𝕜] W)

The space of affine maps between two normed spaces is linearly isometric to the product of the codomain with the space of linear maps, by taking the value of the affine map at (0 : V) and the linear part.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousAffineMap.toConstProdContinuousLinearMap_fst (𝕜 : Type u_1) (V : Type u_2) (W : Type u_3) [NormedAddCommGroup V] [NormedAddCommGroup W] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] (f : V →ᴬ[𝕜] W) : ((toConstProdContinuousLinearMap 𝕜 V W) f).1 = f 0

@[simp]

theorem ContinuousAffineMap.toConstProdContinuousLinearMap_snd (𝕜 : Type u_1) (V : Type u_2) (W : Type u_3) [NormedAddCommGroup V] [NormedAddCommGroup W] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] (f : V →ᴬ[𝕜] W) : ((toConstProdContinuousLinearMap 𝕜 V W) f).2 = f.contLinear