Continuous affine maps between normed spaces. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file develops the theory of continuous affine maps between affine spaces modelled on normed spaces.
In the particular case that the affine spaces are just normed vector spaces V, W, we define a
norm on the space of continuous affine maps by defining the norm of f : V →A[𝕜] W to be
‖f‖ = max ‖f 0‖ ‖f.cont_linear‖. This is chosen so that we have a linear isometry:
(V →A[𝕜] 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: #
def
continuous_affine_map.cont_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
{Q : Type u_7}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f : P →A[R] Q) :
The linear map underlying a continuous affine map is continuous.
Equations
- f.cont_linear = {to_linear_map := {to_fun := ⇑(f.to_affine_map.linear), map_add' := _, map_smul' := _}, cont := _}
@[simp]
theorem
continuous_affine_map.coe_cont_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
{Q : Type u_7}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f : P →A[R] Q) :
⇑(f.cont_linear) = ⇑(f.to_affine_map.linear)
@[simp]
theorem
continuous_affine_map.coe_cont_linear_eq_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
{Q : Type u_7}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f : P →A[R] Q) :
↑(f.cont_linear) = ↑f.linear
@[simp]
theorem
continuous_affine_map.coe_mk_const_linear_eq_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
{Q : Type u_7}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f : P →ᵃ[R] Q)
(h : continuous f.to_fun) :
⇑({to_affine_map := f, cont := h}.cont_linear) = ⇑(f.linear)
theorem
continuous_affine_map.coe_linear_eq_coe_cont_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
{Q : Type u_7}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f : P →A[R] Q) :
@[simp]
theorem
continuous_affine_map.comp_cont_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{W₂ : Type u_5}
{P : Type u_6}
{Q : Type u_7}
{Q₂ : Type u_8}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
[normed_add_comm_group W₂]
[metric_space Q₂]
[normed_add_torsor W₂ Q₂]
[normed_field R]
[normed_space R V]
[normed_space R W]
[normed_space R W₂]
(f : P →A[R] Q)
(g : Q →A[R] Q₂) :
(g.comp f).cont_linear = g.cont_linear.comp f.cont_linear
@[simp]
theorem
continuous_affine_map.map_vadd
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
{Q : Type u_7}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f : P →A[R] Q)
(p : P)
(v : V) :
@[simp]
theorem
continuous_affine_map.cont_linear_map_vsub
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
{Q : Type u_7}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f : P →A[R] Q)
(p₁ p₂ : P) :
@[simp]
theorem
continuous_affine_map.const_cont_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
{Q : Type u_7}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
[normed_field R]
[normed_space R V]
[normed_space R W]
(q : Q) :
(continuous_affine_map.const R P q).cont_linear = 0
theorem
continuous_affine_map.cont_linear_eq_zero_iff_exists_const
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
{Q : Type u_7}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f : P →A[R] Q) :
f.cont_linear = 0 ↔ ∃ (q : Q), f = continuous_affine_map.const R P q
@[simp]
theorem
continuous_affine_map.to_affine_map_cont_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
[normed_add_comm_group V]
[normed_add_comm_group W]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f : V →L[R] W) :
@[simp]
theorem
continuous_affine_map.zero_cont_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[normed_field R]
[normed_space R V]
[normed_space R W] :
0.cont_linear = 0
@[simp]
theorem
continuous_affine_map.add_cont_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f g : P →A[R] W) :
(f + g).cont_linear = f.cont_linear + g.cont_linear
@[simp]
theorem
continuous_affine_map.sub_cont_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f g : P →A[R] W) :
(f - g).cont_linear = f.cont_linear - g.cont_linear
@[simp]
theorem
continuous_affine_map.neg_cont_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f : P →A[R] W) :
(-f).cont_linear = -f.cont_linear
@[simp]
theorem
continuous_affine_map.smul_cont_linear
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
{P : Type u_6}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[normed_field R]
[normed_space R V]
[normed_space R W]
(t : R)
(f : P →A[R] W) :
(t • f).cont_linear = t • f.cont_linear
theorem
continuous_affine_map.decomp
{R : Type u_2}
{V : Type u_3}
{W : Type u_4}
[normed_add_comm_group V]
[normed_add_comm_group W]
[normed_field R]
[normed_space R V]
[normed_space R W]
(f : V →A[R] W) :
⇑f = ⇑(f.cont_linear) + function.const V (⇑f 0)
@[protected, instance]
noncomputable
def
continuous_affine_map.has_norm
{𝕜 : Type u_1}
{V : Type u_3}
{W : Type u_4}
[normed_add_comm_group V]
[normed_add_comm_group W]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 V]
[normed_space 𝕜 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
- continuous_affine_map.has_norm = {norm := λ (f : V →A[𝕜] W), linear_order.max ‖⇑f 0‖ ‖f.cont_linear‖}
theorem
continuous_affine_map.norm_def
{𝕜 : Type u_1}
{V : Type u_3}
{W : Type u_4}
[normed_add_comm_group V]
[normed_add_comm_group W]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 V]
[normed_space 𝕜 W]
(f : V →A[𝕜] W) :
‖f‖ = linear_order.max ‖⇑f 0‖ ‖f.cont_linear‖
theorem
continuous_affine_map.norm_cont_linear_le
{𝕜 : Type u_1}
{V : Type u_3}
{W : Type u_4}
[normed_add_comm_group V]
[normed_add_comm_group W]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 V]
[normed_space 𝕜 W]
(f : V →A[𝕜] W) :
theorem
continuous_affine_map.norm_image_zero_le
{𝕜 : Type u_1}
{V : Type u_3}
{W : Type u_4}
[normed_add_comm_group V]
[normed_add_comm_group W]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 V]
[normed_space 𝕜 W]
(f : V →A[𝕜] W) :
@[simp]
theorem
continuous_affine_map.norm_eq
{𝕜 : Type u_1}
{V : Type u_3}
{W : Type u_4}
[normed_add_comm_group V]
[normed_add_comm_group W]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 V]
[normed_space 𝕜 W]
(f : V →A[𝕜] W)
(h : ⇑f 0 = 0) :
@[protected, instance]
noncomputable
def
continuous_affine_map.normed_add_comm_group
{𝕜 : Type u_1}
{V : Type u_3}
{W : Type u_4}
[normed_add_comm_group V]
[normed_add_comm_group W]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 V]
[normed_space 𝕜 W] :
normed_add_comm_group (V →A[𝕜] W)
Equations
- continuous_affine_map.normed_add_comm_group = {to_fun := λ (f : V →A[𝕜] W), linear_order.max ‖⇑f 0‖ ‖f.cont_linear‖, map_zero' := _, add_le' := _, neg' := _, eq_zero_of_map_eq_zero' := _}.to_normed_add_comm_group
@[protected, instance]
def
continuous_affine_map.normed_space
{𝕜 : Type u_1}
{V : Type u_3}
{W : Type u_4}
[normed_add_comm_group V]
[normed_add_comm_group W]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 V]
[normed_space 𝕜 W] :
normed_space 𝕜 (V →A[𝕜] W)
Equations
- continuous_affine_map.normed_space = {to_module := continuous_affine_map.module continuous_affine_map.normed_space._proof_3, norm_smul_le := _}
theorem
continuous_affine_map.norm_comp_le
{𝕜 : Type u_1}
{V : Type u_3}
{W : Type u_4}
{W₂ : Type u_5}
[normed_add_comm_group V]
[normed_add_comm_group W]
[normed_add_comm_group W₂]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 V]
[normed_space 𝕜 W]
[normed_space 𝕜 W₂]
(f : V →A[𝕜] W)
(g : W₂ →A[𝕜] V) :
def
continuous_affine_map.to_const_prod_continuous_linear_map
(𝕜 : Type u_1)
(V : Type u_3)
(W : Type u_4)
[normed_add_comm_group V]
[normed_add_comm_group W]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 V]
[normed_space 𝕜 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
- continuous_affine_map.to_const_prod_continuous_linear_map 𝕜 V W = {to_linear_equiv := {to_fun := λ (f : V →A[𝕜] W), (⇑f 0, f.cont_linear), map_add' := _, map_smul' := _, inv_fun := λ (p : W × (V →L[𝕜] W)), p.snd.to_continuous_affine_map + continuous_affine_map.const 𝕜 V p.fst, left_inv := _, right_inv := _}, norm_map' := _}
@[simp]
theorem
continuous_affine_map.to_const_prod_continuous_linear_map_fst
(𝕜 : Type u_1)
(V : Type u_3)
(W : Type u_4)
[normed_add_comm_group V]
[normed_add_comm_group W]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 V]
[normed_space 𝕜 W]
(f : V →A[𝕜] W) :
(⇑(continuous_affine_map.to_const_prod_continuous_linear_map 𝕜 V W) f).fst = ⇑f 0
@[simp]
theorem
continuous_affine_map.to_const_prod_continuous_linear_map_snd
(𝕜 : Type u_1)
(V : Type u_3)
(W : Type u_4)
[normed_add_comm_group V]
[normed_add_comm_group W]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 V]
[normed_space 𝕜 W]
(f : V →A[𝕜] W) :