mathlib documentation

analysis.calculus.conformal.inner_product

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

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) :
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) :
inner (f' u) (f' v) = (conformal_factor_at H) * inner u v