Documentation

Mathlib.Analysis.Calculus.Conformal.InnerProduct

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.

source
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.

source
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.

source
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
Instances For
    source
    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
    source
    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⟫_ℝ
    source
    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⟫_ℝ