Conformal maps between inner product spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[normed_add_comm_group E]
[normed_add_comm_group F]
[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}
[normed_add_comm_group E]
[normed_add_comm_group F]
[inner_product_space ℝ E]
[inner_product_space ℝ F]
{f : E → F}
{x : E}
{f' : E →L[ℝ] F}
(h : has_fderiv_at f f' x) :
conformal_at f x ↔ ∃ (c : ℝ), 0 < c ∧ ∀ (u v : E), has_inner.inner (⇑f' u) (⇑f' v) = c * has_inner.inner u v
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}
[normed_add_comm_group E]
[normed_add_comm_group F]
[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}
[normed_add_comm_group E]
[normed_add_comm_group F]
[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}
[normed_add_comm_group E]
[normed_add_comm_group F]
[inner_product_space ℝ E]
[inner_product_space ℝ F]
{f : E → F}
{x : E}
(h : conformal_at f x)
(u v : E) :
has_inner.inner (⇑(fderiv ℝ f x) u) (⇑(fderiv ℝ f x) v) = conformal_factor_at h * has_inner.inner u v
theorem
conformal_factor_at_inner_eq_mul_inner
{E : Type u_1}
{F : Type u_2}
[normed_add_comm_group E]
[normed_add_comm_group F]
[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) :
has_inner.inner (⇑f' u) (⇑f' v) = conformal_factor_at H * has_inner.inner u v