mathlib documentation

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 #

Main results #

In analysis.calculus.conformal.inner_product:

In geometry.euclidean.basic:

Tags #

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] [normed_space X] [normed_space 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] [normed_space X] (x : X) :
theorem conformal_at_const_smul {X : Type u_1} [normed_group X] [normed_space X] {c : } (h : c 0) (x : X) :
conformal_at (λ (x' : X), c x') x
theorem conformal_at_iff_is_conformal_map_fderiv {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [normed_space X] [normed_space 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] [normed_space X] [normed_space Y] {f : X → Y} {x : X} (h : conformal_at f x) :
theorem conformal_at.congr {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [normed_space X] [normed_space Y] {f g : X → Y} {x : X} {u : set X} (hx : x u) (hu : is_open u) (hf : conformal_at f x) (h : ∀ (x : X), x ug x = f 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] [normed_space X] [normed_space Y] [normed_space Z] {f : X → Y} {g : Y → Z} (x : X) (hg : conformal_at g (f x)) (hf : conformal_at f x) :
theorem conformal_at.const_smul {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [normed_space X] [normed_space Y] {f : X → Y} {x : X} {c : } (hc : c 0) (hf : conformal_at f x) :
def conformal {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [normed_space X] [normed_space Y] (f : X → Y) :
Prop

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

Equations
theorem conformal_id {X : Type u_1} [normed_group X] [normed_space X] :
theorem conformal_const_smul {X : Type u_1} [normed_group X] [normed_space 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] [normed_space X] [normed_space Y] {f : X → Y} (h : conformal f) (x : X) :
theorem conformal.differentiable {X : Type u_1} {Y : Type u_2} [normed_group X] [normed_group Y] [normed_space X] [normed_space 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] [normed_space X] [normed_space Y] [normed_space 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] [normed_space X] [normed_space Y] {f : X → Y} (hf : conformal f) {c : } (hc : c 0) :