Conformal maps between inner product spaces #

A function between inner product spaces which has a derivative at x is conformal at x iff the derivative preserves inner products up to a scalar multiple.

theorem conformalAt_iff' {E : Type u_1} {F : Type u_2} [] [] {f : EF} {x : E} :
∃ (c : ), 0 < c ∀ (u v : E), (fderiv f x) u, (fderiv f x) v⟫_ = c * 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 conformalAt_iff {E : Type u_1} {F : Type u_2} [] [] {f : EF} {x : E} {f' : E →L[] F} (h : HasFDerivAt f f' x) :
∃ (c : ), 0 < c ∀ (u v : E), f' u, f' v⟫_ = c * 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 conformalFactorAt {E : Type u_1} {F : Type u_2} [] [] {f : EF} {x : E} (h : ) :

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
Instances For
theorem conformalFactorAt_pos {E : Type u_1} {F : Type u_2} [] [] {f : EF} {x : E} (h : ) :
theorem conformalFactorAt_inner_eq_mul_inner' {E : Type u_1} {F : Type u_2} [] [] {f : EF} {x : E} (h : ) (u : E) (v : E) :
(fderiv f x) u, (fderiv f x) v⟫_ = * u, v⟫_
theorem conformalFactorAt_inner_eq_mul_inner {E : Type u_1} {F : Type u_2} [] [] {f : EF} {x : E} {f' : E →L[] F} (h : HasFDerivAt f f' x) (H : ) (u : E) (v : E) :
f' u, f' v⟫_ = * u, v⟫_