# mathlibdocumentation

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} {f : E → F} {x : E} :
x ∃ (c : ), 0 < c ∀ (u v : E), inner ( f x) u) ( f x) v) = c * 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} {f : E → F} {x : E} {f' : E →L[] F} (h : f' x) :
x ∃ (c : ), 0 < c ∀ (u v : E), inner (f' u) (f' v) = c * 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} {f : E → F} {x : E} (h : 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} {f : E → F} {x : E} (h : x) :
theorem conformal_factor_at_inner_eq_mul_inner' {E : Type u_1} {F : Type u_2} {f : E → F} {x : E} (h : x) (u v : E) :
inner ( f x) u) ( f x) v) = * v
theorem conformal_factor_at_inner_eq_mul_inner {E : Type u_1} {F : Type u_2} {f : E → F} {x : E} {f' : E →L[] F} (h : f' x) (H : x) (u v : E) :
inner (f' u) (f' v) = * v