conformalAt_iff_isConformalMap_fderiv
theorem conformalAt_iff_isConformalMap_fderiv :
∀ {X : Type u_1} {Y : Type u_2} [inst : NormedAddCommGroup X] [inst_1 : NormedAddCommGroup Y]
[inst_2 : NormedSpace ℝ X] [inst_3 : NormedSpace ℝ Y] {f : X → Y} {x : X},
ConformalAt f x ↔ IsConformalMap (fderiv ℝ f x)
This theorem states that a function is a conformal map at a point if and only if its differential at that point is a conformal linear map. In other words, for any function `f` from a real normed additive commutative group `X` to another real normed additive commutative group `Y`, and for any point `x` in `X`, `f` is conformal at `x` if and only if the Fréchet differential of `f` at `x`, denoted `fderiv ℝ f x`, is a conformal linear map.
Remember that a conformal map is one that locally preserves angles and scales (but not necessarily distances), and a conformal linear map is a nonzero multiple of a linear isometry. This theorem connects these two concepts, showing that the property of being a conformal map is equivalent to the property of having a conformal linear map as a derivative.
More concisely: A function between real normed additive commutative groups is conformal at a point if and only if its Fréchet differential at that point is a conformal linear map.
|
ConformalAt.comp
theorem ConformalAt.comp :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : NormedAddCommGroup X] [inst_1 : NormedAddCommGroup Y]
[inst_2 : NormedAddCommGroup Z] [inst_3 : NormedSpace ℝ X] [inst_4 : NormedSpace ℝ Y] [inst_5 : NormedSpace ℝ Z]
{f : X → Y} {g : Y → Z} (x : X), ConformalAt g (f x) → ConformalAt f x → ConformalAt (g ∘ f) x
The theorem `ConformalAt.comp` states that for three types `X`, `Y`, and `Z`, all of which are normed additive commutative groups and normed spaces over the real numbers, if `f` is a map from `X` to `Y` and `g` is a map from `Y` to `Z`, then if `g` is conformal at `f(x)` and `f` is conformal at `x`, the composition of `g` and `f` is also conformal at `x`. In other words, the conformality property is preserved under function composition.
More concisely: If `f: X → Y` and `g: Y → Z` are conformal at `x ∈ X` with respect to normed additive commutative groups and normed spaces over the real numbers, then `g ∘ f` is conformal at `x`.
|