scilib documentation

analysis.calculus.conformal.normed_space

Conformal Maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.angle.unoriented.conformal:

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_add_comm_group X] [normed_add_comm_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_add_comm_group X] [normed_space X] (x : X) :
theorem conformal_at_const_smul {X : Type u_1} [normed_add_comm_group X] [normed_space 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_add_comm_group X] [normed_add_comm_group Y] [normed_space X] [normed_space Y] [subsingleton X] (f : X Y) (x : X) :
theorem conformal_at_iff_is_conformal_map_fderiv {X : Type u_1} {Y : Type u_2} [normed_add_comm_group X] [normed_add_comm_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_add_comm_group X] [normed_add_comm_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_add_comm_group X] [normed_add_comm_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 u g x = f x) :
theorem conformal_at.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [normed_add_comm_group X] [normed_add_comm_group Y] [normed_add_comm_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_add_comm_group X] [normed_add_comm_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_add_comm_group X] [normed_add_comm_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_const_smul {X : Type u_1} [normed_add_comm_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_add_comm_group X] [normed_add_comm_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_add_comm_group X] [normed_add_comm_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_add_comm_group X] [normed_add_comm_group Y] [normed_add_comm_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_add_comm_group X] [normed_add_comm_group Y] [normed_space X] [normed_space Y] {f : X Y} (hf : conformal f) {c : } (hc : c 0) :