/
InnerProduct.lean
60 lines (47 loc) · 2.91 KB
/
InnerProduct.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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
/-
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.Calculus.Conformal.NormedSpace
import Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
#align_import analysis.calculus.conformal.inner_product from "leanprover-community/mathlib"@"46b633fd842bef9469441c0209906f6dddd2b4f5"
/-!
# Conformal maps between inner product spaces
A function between inner product spaces which has a derivative at `x`
is conformal at `x` iff the derivative preserves inner products up to a scalar multiple.
-/
noncomputable section
variable {E F : Type*}
variable [NormedAddCommGroup E] [NormedAddCommGroup F]
variable [InnerProductSpace ℝ E] [InnerProductSpace ℝ F]
open RealInnerProductSpace
/-- A real differentiable map `f` is conformal at point `x` if and only if its
differential `fderiv ℝ f x` at that point scales every inner product by a positive scalar. -/
theorem conformalAt_iff' {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⟫ :=
by rw [conformalAt_iff_isConformalMap_fderiv, isConformalMap_iff]
#align conformal_at_iff' conformalAt_iff'
/-- 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]
#align conformal_at_iff conformalAt_iff
/-- The conformal factor of a conformal map at some point `x`. Some authors refer to this function
as the characteristic function of the conformal map. -/
def conformalFactorAt {f : E → F} {x : E} (h : ConformalAt f x) : ℝ :=
Classical.choose (conformalAt_iff'.mp h)
#align conformal_factor_at conformalFactorAt
theorem conformalFactorAt_pos {f : E → F} {x : E} (h : ConformalAt f x) : 0 < conformalFactorAt h :=
(Classical.choose_spec <| conformalAt_iff'.mp h).1
#align conformal_factor_at_pos conformalFactorAt_pos
theorem conformalFactorAt_inner_eq_mul_inner' {f : E → F} {x : E} (h : ConformalAt f x) (u v : E) :
⟪(fderiv ℝ f x) u, (fderiv ℝ f x) v⟫ = (conformalFactorAt h : ℝ) * ⟪u, v⟫ :=
(Classical.choose_spec <| conformalAt_iff'.mp h).2 u v
#align conformal_factor_at_inner_eq_mul_inner' conformalFactorAt_inner_eq_mul_inner'
theorem conformalFactorAt_inner_eq_mul_inner {f : E → F} {x : E} {f' : E →L[ℝ] F}
(h : HasFDerivAt f f' x) (H : ConformalAt f x) (u v : E) :
⟪f' u, f' v⟫ = (conformalFactorAt H : ℝ) * ⟪u, v⟫ :=
H.differentiableAt.hasFDerivAt.unique h ▸ conformalFactorAt_inner_eq_mul_inner' H u v
#align conformal_factor_at_inner_eq_mul_inner conformalFactorAt_inner_eq_mul_inner