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} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] {f : E → F} {x : E} : ConformalAt f x ↔ ∃ (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} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] {f : E → F} {x : E} {f' : E →L[ℝ] F} (h : HasFDerivAt f f' x) : ConformalAt 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} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] {f : E → F} {x : E} (h : ConformalAt 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

• conformalFactorAt h = Classical.choose (_ : ∃ (c : ℝ), 0 < c ∧ ∀ (u v : E), ⟪(fderiv ℝ f x) u, (fderiv ℝ f x) v⟫_ℝ = c * ⟪u, v⟫_ℝ)

theorem conformalFactorAt_pos {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] {f : E → F} {x : E} (h : ConformalAt f x) : 0 < conformalFactorAt h

theorem conformalFactorAt_inner_eq_mul_inner' {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] {f : E → F} {x : E} (h : ConformalAt f x) (u : E) (v : E) : ⟪(fderiv ℝ f x) u, (fderiv ℝ f x) v⟫_ℝ = conformalFactorAt h * ⟪u, v⟫_ℝ

theorem conformalFactorAt_inner_eq_mul_inner {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] {f : E → F} {x : E} {f' : E →L[ℝ] F} (h : HasFDerivAt f f' x) (H : ConformalAt f x) (u : E) (v : E) : ⟪f' u, f' v⟫_ℝ = conformalFactorAt H * ⟪u, v⟫_ℝ