Documentation

TauCeti.Geometry.Manifold.Diffeomorph.NormedSpace

Elementary diffeomorphisms of a normed space #

The map x ↦ a - x of a normed space E is a diffeomorphism of E, of any smoothness, which is its own inverse (Diffeomorph.subLeft, the smooth counterpart of Equiv.subLeft). On the real line, Diffeomorph.subLeft 1 is the reflection t ↦ 1 - t exchanging 0 and 1.

A continuous linear equivalence of normed spaces is a diffeomorphism of every smoothness (ContinuousLinearEquiv.toContDiffDiffeomorph). Mathlib's ContinuousLinearEquiv.toDiffeomorph provides only the C^∞ one.

For a nonzero scalar a, the affine map x ↦ a • x + b is a diffeomorphism of E, of any smoothness, with inverse y ↦ a⁻¹ • (y - b) (Diffeomorph.smulAdd). On the real line these are the affine changes of time t ↦ a * t + b.

A diffeomorphism between normed spaces of nonzero smoothness is differentiable (Diffeomorph.differentiable), and its Fréchet derivative composed with that of its inverse is the identity (Diffeomorph.fderiv_apply_fderiv_symm_apply).

source
theorem Diffeomorph.differentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) (hn : n ≠ 0) :
Differentiable 𝕜 ⇑h

A diffeomorphism between normed spaces of nonzero smoothness is differentiable.

source
@[simp]
theorem Diffeomorph.fderiv_apply_fderiv_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) (hn : n ≠ 0) (x v : F) :
(fderiv 𝕜 (⇑h) (h.symm x)) ((fderiv 𝕜 (⇑h.symm) x) v) = v

The derivatives of a normed-space diffeomorphism and its inverse compose to the identity.

source
def Diffeomorph.subLeft (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (n : WithTop ℕ∞) (a : E) :
Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) E E n

The map x ↦ a - x of a normed space, as a diffeomorphism. It is its own inverse (Diffeomorph.symm_subLeft).

Instances For
    source
    @[simp]
    theorem Diffeomorph.subLeft_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} (a x : E) :
    (subLeft 𝕜 n a) x = a - x

    Diffeomorph.subLeft 𝕜 n a sends x to a - x.

    source
    @[simp]
    theorem Diffeomorph.symm_subLeft {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} (a : E) :
    (subLeft 𝕜 n a).symm = subLeft 𝕜 n a

    Diffeomorph.subLeft 𝕜 n a is its own inverse.

    source
    def Diffeomorph.smulAdd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (n : WithTop ℕ∞) (a : 𝕜) (b : E) (ha : a ≠ 0) :
    Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) E E n

    The affine map x ↦ a • x + b of a normed space, for a nonzero scalar a, as a diffeomorphism.

    Instances For
      source
      @[simp]
      theorem Diffeomorph.smulAdd_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} (a : 𝕜) (b : E) (ha : a ≠ 0) (x : E) :
      (smulAdd n a b ha) x = a • x + b

      Diffeomorph.smulAdd n a b ha sends x to a • x + b.

      source
      @[simp]
      theorem Diffeomorph.smulAdd_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} (a : 𝕜) (b : E) (ha : a ≠ 0) (y : E) :
      (smulAdd n a b ha).symm y = a⁻¹ • (y - b)

      The inverse of Diffeomorph.smulAdd n a b ha sends y to a⁻¹ • (y - b).

      source
      def ContinuousLinearEquiv.toContDiffDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (L : E ≃L[𝕜] F) (n : WithTop ℕ∞) :
      Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n

      A continuous linear equivalence of normed spaces, as a C^n diffeomorphism for any smoothness exponent n. Mathlib's ContinuousLinearEquiv.toDiffeomorph is the C^∞ one.

      Instances For
        source
        @[simp]
        theorem ContinuousLinearEquiv.coe_toContDiffDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (L : E ≃L[𝕜] F) (n : WithTop ℕ∞) :
        ⇑(L.toContDiffDiffeomorph n) = ⇑L

        L.toContDiffDiffeomorph n is L.

        source
        @[simp]
        theorem ContinuousLinearEquiv.symm_toContDiffDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (L : E ≃L[𝕜] F) (n : WithTop ℕ∞) :
        L.symm.toContDiffDiffeomorph n = (L.toContDiffDiffeomorph n).symm

        The diffeomorphism of L.symm is the inverse of the diffeomorphism of L.

        source
        @[simp]
        theorem ContinuousLinearEquiv.coe_toContDiffDiffeomorph_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (L : E ≃L[𝕜] F) (n : WithTop ℕ∞) :
        ⇑(L.toContDiffDiffeomorph n).symm = ⇑L.symm

        The inverse of L.toContDiffDiffeomorph n is L.symm.