English
The conformal factor at a point is the scalar c such that all inner products after applying f' are scaled by c.
Русский
Конформальный множитель в точке — это скаляр c, который масштабирует все скалярные произведения после применения дифференциала f'.
LaTeX
$$$ \text{conformalFactorAt}(h) = c \text{ where } \forall u,v, \langle f'(x)u, f'(x)v \rangle = c \langle u,v \rangle $$$
Lean4
/-- 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. -/
theorem conformalAt_iff {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⟫ := by simp only [conformalAt_iff', h.fderiv]
