mathlib3 documentation

analysis.calculus.conformal.inner_product

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} :
conformal_at f x (c : ), 0 < c (u v : E), has_inner.inner ((fderiv f x) u) ((fderiv f x) v) = c * has_inner.inner u v

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