English
A linear map f between real inner product spaces is conformal if and only if there exists a positive c such that the inner product is scaled by c, i.e., ⟪f u, f v⟫ = c ⟪u, v⟫ for all u,v.
Русский
Линейное отображение между вещественными пространствами с внутренним произведением конформно тогда и только тогда, когда существует положительный коэффициент c, который масштабирует скалярное произведение: ⟪f u, f v⟫ = c ⟪u, v⟫ для всех u, v.
LaTeX
$$$\\text{IsConformalMap } f \\iff \\exists c>0, \\ \\forall u,v,\\ ⟪f u, f v\\rangle = c\\,⟪u,v⟫$$$
Lean4
/-- A map between two inner product spaces is a conformal map if and only if it preserves inner
products up to a scalar factor, i.e., there exists a positive `c : ℝ` such that
`⟪f u, f v⟫ = c * ⟪u, v⟫` for all `u`, `v`. -/
theorem isConformalMap_iff (f : E →L[ℝ] F) : IsConformalMap f ↔ ∃ c : ℝ, 0 < c ∧ ∀ u v : E, ⟪f u, f v⟫ = c * ⟪u, v⟫ :=
by
constructor
· rintro ⟨c₁, hc₁, li, rfl⟩
refine ⟨c₁ * c₁, mul_self_pos.2 hc₁, fun u v => ?_⟩
simp only [real_inner_smul_left, real_inner_smul_right, mul_assoc, coe_smul', coe_toContinuousLinearMap,
Pi.smul_apply, inner_map_map]
· rintro ⟨c₁, hc₁, huv⟩
obtain ⟨c, hc, rfl⟩ : ∃ c : ℝ, 0 < c ∧ c₁ = c * c := ⟨√c₁, Real.sqrt_pos.2 hc₁, (Real.mul_self_sqrt hc₁.le).symm⟩
refine ⟨c, hc.ne', (c⁻¹ • f : E →ₗ[ℝ] F).isometryOfInner fun u v => ?_, ?_⟩
·
simp only [real_inner_smul_left, real_inner_smul_right, huv, mul_assoc, inv_mul_cancel_left₀ hc.ne',
LinearMap.smul_apply, ContinuousLinearMap.coe_coe]
· ext1 x
exact (smul_inv_smul₀ hc.ne' (f x)).symm
