# mathlibdocumentation

analysis.calculus.conformal.normed_space

# Conformal Maps #

A continuous linear map between real normed spaces X and Y is conformal_at some point x if it is real differentiable at that point and its differential is_conformal_linear_map.

## Main definitions #

• conformal_at: the main definition of conformal maps
• conformal: maps that are conformal at every point
• conformal_factor_at: the conformal factor of a conformal map at some point

## Main results #

• The conformality of the composition of two conformal maps, the identity map and multiplications by nonzero constants
• conformal_at_iff_is_conformal_map_fderiv: an equivalent definition of the conformality of a map

In analysis.calculus.conformal.inner_product:

• conformal_at_iff: an equivalent definition of the conformality of a map

In geometry.euclidean.basic:

• conformal_at.preserves_angle: if a map is conformal at x, then its differential preserves all angles at x

conformal

## Warning #

The definition of conformality in this file does NOT require the maps to be orientation-preserving. Maps such as the complex conjugate are considered to be conformal.

def conformal_at {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [ X] [ Y] (f : X → Y) (x : X) :
Prop

A map f is said to be conformal if it has a conformal differential f'.

Equations
theorem conformal_at_id {X : Type u_1} [normed_group X] [ X] (x : X) :
theorem conformal_at_const_smul {X : Type u_1} [normed_group X] [ X] {c : } (h : c 0) (x : X) :
conformal_at (λ (x' : X), c x') x
theorem subsingleton.conformal_at {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [ X] [ Y] [subsingleton X] (f : X → Y) (x : X) :
x
theorem conformal_at_iff_is_conformal_map_fderiv {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [ X] [ Y] {f : X → Y} {x : X} :

A function is a conformal map if and only if its differential is a conformal linear map

theorem conformal_at.differentiable_at {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [ X] [ Y] {f : X → Y} {x : X} (h : x) :
theorem conformal_at.congr {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [ X] [ Y] {f g : X → Y} {x : X} {u : set X} (hx : x u) (hu : is_open u) (hf : x) (h : ∀ (x : X), x ug x = f x) :
x
theorem conformal_at.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [normed_group X] [normed_group Y] [normed_group Z] [ X] [ Y] [ Z] {f : X → Y} {g : Y → Z} (x : X) (hg : (f x)) (hf : x) :
theorem conformal_at.const_smul {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [ X] [ Y] {f : X → Y} {x : X} {c : } (hc : c 0) (hf : x) :
def conformal {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [ X] [ Y] (f : X → Y) :
Prop

A map f is conformal if it's conformal at every point.

Equations
• = ∀ (x : X), x
theorem conformal_id {X : Type u_1} [normed_group X] [ X] :
theorem conformal_const_smul {X : Type u_1} [normed_group X] [ X] {c : } (h : c 0) :
conformal (λ (x : X), c x)
theorem conformal.conformal_at {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [ X] [ Y] {f : X → Y} (h : conformal f) (x : X) :
x
theorem conformal.differentiable {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [ X] [ Y] {f : X → Y} (h : conformal f) :
theorem conformal.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [normed_group X] [normed_group Y] [normed_group Z] [ X] [ Y] [ Z] {f : X → Y} {g : Y → Z} (hf : conformal f) (hg : conformal g) :
theorem conformal.const_smul {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [ X] [ Y] {f : X → Y} (hf : conformal f) {c : } (hc : c 0) :