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 #

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

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

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

conformal_at f x = ∃ (f' : X →L[ℝ ] Y), has_fderiv_at f f' x ∧ is_conformal_map f'

theorem conformal_at_id {X : Type u_1} [normed_add_comm_group X] [normed_space ℝ X] (x : X) :

conformal_at id 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) :

conformal_at f 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} :

conformal_at f x ↔ is_conformal_map (fderiv ℝ f 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) :

differentiable_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) :

conformal_at g 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) :

conformal_at (g ∘ 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) :

conformal_at (c • 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

conformal f = ∀ (x : X), conformal_at f x

theorem conformal_id {X : Type u_1} [normed_add_comm_group X] [normed_space ℝ X] :

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) :

conformal_at f 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) :

differentiable ℝ 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) :

conformal (g ∘ f)

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) :

conformal (c • f)