Conformal maps between inner product spaces #
A function between inner product spaces is which has a derivative at x
is conformal at x iff the derivative preserves inner products up to a scalar multiple.
theorem
conformal_at_iff'
{E : Type u_1}
{F : Type u_2}
[inner_product_space ℝ E]
[inner_product_space ℝ F]
{f : E → F}
{x : E} :
A real differentiable map f is conformal at point x if and only if its
differential fderiv ℝ f x at that point scales every inner product by a positive scalar.
theorem
conformal_at_iff
{E : Type u_1}
{F : Type u_2}
[inner_product_space ℝ E]
[inner_product_space ℝ F]
{f : E → F}
{x : E}
{f' : E →L[ℝ] F}
(h : has_fderiv_at f f' x) :
A real differentiable map f is conformal at point x if and only if its
differential f' at that point scales every inner product by a positive scalar.
noncomputable
def
conformal_factor_at
{E : Type u_1}
{F : Type u_2}
[inner_product_space ℝ E]
[inner_product_space ℝ F]
{f : E → F}
{x : E}
(h : conformal_at f x) :
The conformal factor of a conformal map at some point x. Some authors refer to this function
as the characteristic function of the conformal map.
Equations
theorem
conformal_factor_at_pos
{E : Type u_1}
{F : Type u_2}
[inner_product_space ℝ E]
[inner_product_space ℝ F]
{f : E → F}
{x : E}
(h : conformal_at f x) :
0 < conformal_factor_at h
theorem
conformal_factor_at_inner_eq_mul_inner'
{E : Type u_1}
{F : Type u_2}
[inner_product_space ℝ E]
[inner_product_space ℝ F]
{f : E → F}
{x : E}
(h : conformal_at f x)
(u v : E) :
theorem
conformal_factor_at_inner_eq_mul_inner
{E : Type u_1}
{F : Type u_2}
[inner_product_space ℝ E]
[inner_product_space ℝ F]
{f : E → F}
{x : E}
{f' : E →L[ℝ] F}
(h : has_fderiv_at f f' x)
(H : conformal_at f x)
(u v : E) :