Affine isometries

For a scalar c and an affine isometry e : V ≃ᵃⁱ[𝕜] V₂ between normed spaces, the affine isometry TauCeti.dilateConj c e has the linear part of e and translation part c • e 0. For c ≠ 0 it is the conjugate y ↦ c • e (c⁻¹ • y) of e by the dilations by c.

The derivative of an affine isometry equivalence has norm at most one.

Main declarations

• TauCeti.dilateConj: the dilation conjugate of an affine isometry.
• TauCeti.dilateConj_smul: dilateConj c e (c • y) = c • e y.
• TauCeti.dilateConj_symm_apply: the inverse of dilateConj c e, written out pointwise.
• AffineIsometryEquiv.norm_fderiv_le: the derivative of an affine isometry equivalence has norm at most one.

theorem AffineIsometryEquiv.norm_fderiv_le {𝕜 : Type u_1} {W : Type u_2} {W₂ : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup W] [NormedSpace 𝕜 W] [NormedAddCommGroup W₂] [NormedSpace 𝕜 W₂] (e : W ≃ᵃⁱ[𝕜] W₂) (x : W) : ‖fderiv 𝕜 (⇑e) x‖ ≤ 1

The Fréchet derivative of an affine isometry equivalence has norm at most one.

def TauCeti.dilateConj {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] (c : 𝕜) (e : V ≃ᵃⁱ[𝕜] V₂) : V ≃ᵃⁱ[𝕜] V₂

The affine isometry with the linear part of e and translation part c • e 0. For c ≠ 0 it is the conjugate y ↦ c • e (c⁻¹ • y) of e by the dilation by c; for c = 0 it is the linear part of e.

@[simp]

theorem TauCeti.dilateConj_smul {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] (c : 𝕜) (e : V ≃ᵃⁱ[𝕜] V₂) (y : V) : (dilateConj c e) (c • y) = c • e y

The dilation conjugate of e sends c • y to c • e y.

theorem TauCeti.dilateConj_symm_apply {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] {c : 𝕜} (hc : c ≠ 0) (e : V ≃ᵃⁱ[𝕜] V₂) (z : V₂) : (dilateConj c e).symm z = c • e.symm (c⁻¹ • z)

The inverse of the dilation conjugate of e by c ≠ 0 is the dilation conjugate of e.symm, written out pointwise.