# mathlib3documentation

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

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), has_inner.inner (f' u) (f' v) = c *

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} {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) :
has_inner.inner ( f x) u) ( f x) 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) :
has_inner.inner (f' u) (f' v) =