Documentation

Mathlib.Analysis.NormedSpace.ConformalLinearMap

Conformal Linear Maps #

A continuous linear map between R-normed spaces X and Y IsConformalMap if it is a nonzero multiple of a linear isometry.

Main definitions #

Main results #

See Analysis.InnerProductSpace.ConformalLinearMap for

Tags #

conformal

Warning #

The definition of conformality in this file does NOT require the maps to be orientation-preserving.

def IsConformalMap {R : Type u_1} {X : Type u_2} {Y : Type u_3} [NormedField R] [SeminormedAddCommGroup X] [SeminormedAddCommGroup Y] [NormedSpace R X] [NormedSpace R Y] (f' : X →L[R] Y) :

A continuous linear map f' is said to be conformal if it's a nonzero multiple of a linear isometry.

Equations
Instances For
    theorem IsConformalMap.smul {R : Type u_1} {M : Type u_2} {N : Type u_3} [NormedField R] [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] [NormedSpace R M] [NormedSpace R N] {f : M →L[R] N} (hf : IsConformalMap f) {c : R} (hc : c 0) :
    theorem LinearIsometry.isConformalMap {R : Type u_1} {M : Type u_2} {N : Type u_3} [NormedField R] [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] [NormedSpace R M] [NormedSpace R N] (f' : M →ₗᵢ[R] N) :
    IsConformalMap f'.toContinuousLinearMap
    theorem IsConformalMap.comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {G : Type u_4} [NormedField R] [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] [SeminormedAddCommGroup G] [NormedSpace R M] [NormedSpace R N] [NormedSpace R G] {f : M →L[R] N} {g : N →L[R] G} (hg : IsConformalMap g) (hf : IsConformalMap f) :
    IsConformalMap (g.comp f)
    theorem IsConformalMap.injective {R : Type u_1} {N : Type u_3} {M' : Type u_5} [NormedField R] [SeminormedAddCommGroup N] [NormedSpace R N] [NormedAddCommGroup M'] [NormedSpace R M'] {f : M' →L[R] N} (h : IsConformalMap f) :
    theorem IsConformalMap.ne_zero {R : Type u_1} {N : Type u_3} {M' : Type u_5} [NormedField R] [SeminormedAddCommGroup N] [NormedSpace R N] [NormedAddCommGroup M'] [NormedSpace R M'] [Nontrivial M'] {f' : M' →L[R] N} (hf' : IsConformalMap f') :
    f' 0