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 #
conformal_at
: the main definition of conformal mapsconformal
: maps that are conformal at every pointconformal_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 atx
, then its differential preserves all angles atx
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_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_const_smul
{X : Type u_1}
[normed_add_comm_group X]
[normed_space ℝ X]
{c : ℝ}
(h : c ≠ 0) :
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) :
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) :