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), inner ℝ ((fderiv ℝ f x) u) ((fderiv ℝ f x) v) = c * inner ℝ 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), inner ℝ (f' u) (f' v) = c * inner ℝ 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
noncomputable 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 v : E) :
    inner ℝ ((fderiv ℝ f x) u) ((fderiv ℝ f x) v) = conformalFactorAt h * inner ℝ 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 v : E) :
    inner ℝ (f' u) (f' v) = conformalFactorAt H * inner ℝ u v