Conformal Maps #

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

Main definitions #

• ConformalAt: the main definition of conformal maps
• Conformal: maps that are conformal at every point

Main results #

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

In Analysis.Calculus.Conformal.InnerProduct:

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

In Geometry.Euclidean.Angle.Unoriented.Conformal:

• ConformalAt.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 ConformalAt {X : Type u_1} {Y : Type u_2} [] [] (f : XY) (x : X) :

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

Equations
Instances For
theorem conformalAt_id {X : Type u_1} [] (x : X) :
theorem conformalAt_const_smul {X : Type u_1} [] {c : } (h : c 0) (x : X) :
ConformalAt (fun (x' : X) => c x') x
theorem Subsingleton.conformalAt {X : Type u_1} {Y : Type u_2} [] [] [] (f : XY) (x : X) :
theorem conformalAt_iff_isConformalMap_fderiv {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} :

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

theorem ConformalAt.differentiableAt {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} (h : ) :
theorem ConformalAt.congr {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {g : XY} {x : X} {u : Set X} (hx : x u) (hu : ) (hf : ) (h : xu, g x = f x) :
theorem ConformalAt.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : XY} {g : YZ} (x : X) (hg : ConformalAt g (f x)) (hf : ) :
theorem ConformalAt.const_smul {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} {c : } (hc : c 0) (hf : ) :
def Conformal {X : Type u_1} {Y : Type u_2} [] [] (f : XY) :

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

Equations
• = ∀ (x : X),
Instances For
theorem conformal_id {X : Type u_1} [] :
theorem conformal_const_smul {X : Type u_1} [] {c : } (h : c 0) :
Conformal fun (x : X) => c x
theorem Conformal.conformalAt {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (h : ) (x : X) :
theorem Conformal.differentiable {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (h : ) :
theorem Conformal.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : XY} {g : YZ} (hf : ) (hg : ) :
theorem Conformal.const_smul {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) {c : } (hc : c 0) :