conformalAt_iff
theorem conformalAt_iff :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
[inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {f : E → F} {x : E} {f' : E →L[ℝ] F},
HasFDerivAt f f' x → (ConformalAt f x ↔ ∃ c, 0 < c ∧ ∀ (u v : E), ⟪f' u, f' v⟫_ℝ = c * ⟪u, v⟫_ℝ)
This theorem states that for a real-valued differentiable function `f`, the function is conformal at a point `x` if and only if its derivative `f'` at that point scales every inner product by a positive scalar. In more detail, given a normed addtive commutative group `E` and `F` both with inner product space structure over the real numbers, a function `f` from `E` to `F`, a point `x` in `E` and a continuous linear map `f'` from `E` to `F`, if `f` has its derivative `f'` at `x`, then `f` is conformal at `x` if and only if there exists a positive real number `c` such that for all vectors `u` and `v` in `E`, the inner product of `f' u` and `f' v` is equal to `c` times the inner product of `u` and `v`.
More concisely: A real-valued differentiable function `f` is conformal at a point `x` if and only if its derivative `f'` at `x` scales every inner product by a positive scalar. That is, there exists a positive real number `c` such that for all vectors `u` and `v` in the domain of `f`, the inner product of `f' u` and `f' v` equals `c` times the inner product of `u` and `v`.
|
conformalAt_iff'
theorem conformalAt_iff' :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
[inst_2 : InnerProductSpace ℝ E] [inst_3 : 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⟫_ℝ
The theorem `conformalAt_iff'` states that for a given real differentiable map `f` from a normed additive commutative group `E` equipped with an inner product space over the real numbers to another such group `F`, `f` is conformal at a point `x` if and only if the derivative of `f` at that point, represented by `fderiv ℝ f x`, scales every inner product of `u` and `v` (where `u` and `v` are elements of `E`) by a positive scalar `c`. In mathematical terms, this is expressed as `⟪(fderiv ℝ f x) u, (fderiv ℝ f x) v⟫_ℝ = c * ⟪u, v⟫_ℝ` for some `c` greater than zero.
More concisely: A real differentiable map `f` from one inner product space to another scales inner products at a point `x` by a positive scalar if and only if the derivative of `f` at `x` is conformal, i.e., `⟪(fderiv ℝ f x) u, (fderiv ℝ f x) v⟫_ℝ = c * ⟪u, v⟫_ℝ` for some positive scalar `c`.
|