-
Notifications
You must be signed in to change notification settings - Fork 251
/
ConformalLinearMap.lean
44 lines (36 loc) · 1.93 KB
/
ConformalLinearMap.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
/-
Copyright (c) 2021 Yourong Zang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yourong Zang
-/
import Mathlib.Analysis.NormedSpace.ConformalLinearMap
import Mathlib.Analysis.InnerProductSpace.Basic
#align_import analysis.inner_product_space.conformal_linear_map from "leanprover-community/mathlib"@"46b633fd842bef9469441c0209906f6dddd2b4f5"
/-!
# Conformal maps between inner product spaces
In an inner product space, a map is conformal iff it preserves inner products up to a scalar factor.
-/
variable {E F : Type*}
variable [NormedAddCommGroup E] [NormedAddCommGroup F]
variable [InnerProductSpace ℝ E] [InnerProductSpace ℝ F]
open LinearIsometry ContinuousLinearMap
open RealInnerProductSpace
/-- 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, coe_smul,
inv_mul_cancel_left₀ hc.ne', LinearMap.smul_apply, ContinuousLinearMap.coe_coe]
· ext1 x
exact (smul_inv_smul₀ hc.ne' (f x)).symm
#align is_conformal_map_iff isConformalMap_iff