mathlib documentation

analysis.normed_space.conformal_linear_map

Conformal Linear Maps #

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

Main definitions #

Main results #

See analysis.normed_space.conformal_linear_map.inner_product for

Tags #

conformal

Warning #

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

def is_conformal_map {R : Type u_1} {X : Type u_2} {Y : Type u_3} [normed_field R] [seminormed_add_comm_group X] [seminormed_add_comm_group Y] [normed_space R X] [normed_space R Y] (f' : X →L[R] Y) :
Prop

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

Equations
theorem is_conformal_map.smul {R : Type u_1} {M : Type u_2} {N : Type u_3} [normed_field R] [seminormed_add_comm_group M] [seminormed_add_comm_group N] [normed_space R M] [normed_space R N] {f : M →L[R] N} (hf : is_conformal_map f) {c : R} (hc : c 0) :
theorem is_conformal_map_const_smul {R : Type u_1} {M : Type u_2} [normed_field R] [seminormed_add_comm_group M] [normed_space R M] {c : R} (hc : c 0) :
@[protected]
theorem is_conformal_map_of_subsingleton {R : Type u_1} {M : Type u_2} {N : Type u_3} [normed_field R] [seminormed_add_comm_group M] [seminormed_add_comm_group N] [normed_space R M] [normed_space R N] [subsingleton M] (f' : M →L[R] N) :
theorem is_conformal_map.comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {G : Type u_4} [normed_field R] [seminormed_add_comm_group M] [seminormed_add_comm_group N] [seminormed_add_comm_group G] [normed_space R M] [normed_space R N] [normed_space R G] {f : M →L[R] N} {g : N →L[R] G} (hg : is_conformal_map g) (hf : is_conformal_map f) :
@[protected]
theorem is_conformal_map.injective {R : Type u_1} {N : Type u_3} {M' : Type u_5} [normed_field R] [seminormed_add_comm_group N] [normed_space R N] [normed_add_comm_group M'] [normed_space R M'] {f : M' →L[R] N} (h : is_conformal_map f) :
theorem is_conformal_map.ne_zero {R : Type u_1} {N : Type u_3} {M' : Type u_5} [normed_field R] [seminormed_add_comm_group N] [normed_space R N] [normed_add_comm_group M'] [normed_space R M'] [nontrivial M'] {f' : M' →L[R] N} (hf' : is_conformal_map f') :
f' 0