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

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 ConformalAt {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedSpace ℝ X] [NormedSpace ℝ Y] (f : X → Y) (x : X) : Prop

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

Equations

• ConformalAt f x = ∃ (f' : X →L[ℝ] Y), HasFDerivAt f f' x ∧ IsConformalMap f'

theorem conformalAt_id {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (x : X) : ConformalAt id x

theorem conformalAt_const_smul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {c : ℝ} (h : c ≠ 0) (x : X) : ConformalAt (fun (x' : X) => c • x') x

theorem Subsingleton.conformalAt {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedSpace ℝ X] [NormedSpace ℝ Y] [Subsingleton X] (f : X → Y) (x : X) : ConformalAt f x

theorem conformalAt_iff_isConformalMap_fderiv {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedSpace ℝ X] [NormedSpace ℝ Y] {f : X → Y} {x : X} : ConformalAt f x ↔ IsConformalMap (fderiv ℝ f 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} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedSpace ℝ X] [NormedSpace ℝ Y] {f : X → Y} {x : X} (h : ConformalAt f x) : DifferentiableAt ℝ f x

theorem ConformalAt.congr {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedSpace ℝ X] [NormedSpace ℝ Y] {f : X → Y} {g : X → Y} {x : X} {u : Set X} (hx : x ∈ u) (hu : IsOpen u) (hf : ConformalAt f x) (h : ∀ x ∈ u, g x = f x) : ConformalAt g x

theorem ConformalAt.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedAddCommGroup Z] [NormedSpace ℝ X] [NormedSpace ℝ Y] [NormedSpace ℝ Z] {f : X → Y} {g : Y → Z} (x : X) (hg : ConformalAt g (f x)) (hf : ConformalAt f x) : ConformalAt (g ∘ f) x

theorem ConformalAt.const_smul {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedSpace ℝ X] [NormedSpace ℝ Y] {f : X → Y} {x : X} {c : ℝ} (hc : c ≠ 0) (hf : ConformalAt f x) : ConformalAt (c • f) x

def Conformal {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedSpace ℝ X] [NormedSpace ℝ Y] (f : X → Y) : Prop

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

Equations

• Conformal f = ∀ (x : X), ConformalAt f x

theorem conformal_id {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : Conformal id

theorem conformal_const_smul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {c : ℝ} (h : c ≠ 0) : Conformal fun (x : X) => c • x

theorem Conformal.conformalAt {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedSpace ℝ X] [NormedSpace ℝ Y] {f : X → Y} (h : Conformal f) (x : X) : ConformalAt f x

theorem Conformal.differentiable {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedSpace ℝ X] [NormedSpace ℝ Y] {f : X → Y} (h : Conformal f) : Differentiable ℝ f

theorem Conformal.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedAddCommGroup Z] [NormedSpace ℝ X] [NormedSpace ℝ Y] [NormedSpace ℝ 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} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedSpace ℝ X] [NormedSpace ℝ Y] {f : X → Y} (hf : Conformal f) {c : ℝ} (hc : c ≠ 0) : Conformal (c • f)