ProjectedCurvature.lean

1 module
2 public import Mathlib.Analysis.Calculus.VectorField
3 public import Mathlib.Analysis.Calculus.FDeriv.Mul
4 public import Mathlib.Analysis.Calculus.FDeriv.CompCLM
5 public import Mathlib.Analysis.Normed.Operator.Mul
6 public import Mathlib.Tactic
7 /-! Author: Komorebi P. Paper VII, fourth block.
8 Actual Frechet derivatives and actual vector fields, including the Lie bracket.
9 This is a parameter-space/chart formalization; it does not construct a global
10 smooth range bundle over an arbitrary manifold. -/
11 public section
12 set_option autoImplicit false
13 set_option backward.isDefEq.respectTransparency false
14 set_option backward.isDefEq.respectTransparency.types false
15 set_option linter.unusedSectionVars false
16 namespace KomorebiPaperVII.Curvature
17 open scoped ContDiff
18 
19 section Algebra
20 variable {R : Type*} [Ring R]
21 /-- Derived differentiated-idempotent consequence, not an assumed zero block. -/
22 theorem jet_sandwich_zero (P D : R) (hP : P*P=P)
23     (hD : D*P+P*D=D) : P*D*P=0 := by
24   have hh := congrArg (fun z => P*z) hD
25   simp only [mul_add, ← mul_assoc, hP] at hh
26   exact add_eq_right.mp hh
27 end Algebra
28 
29 variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
30   [NormedAddCommGroup F] [NormedSpace ℝ F]
31 
32 /-- Projected differentiation along a parameter-space vector field. -/
33 noncomputable def nabla (P : E → F →L[ℝ] F) (X : E → E) (s : E → F) (x : E) : F :=
34   P x (fderiv ℝ s x (X x))
35 
36 /-- The actual covariant commutator, including the vector-field bracket. -/
37 noncomputable def curvature (P : E → F →L[ℝ] F) (X Y : E → E)
38     (s : E → F) (x : E) : F :=
39   nabla P X (nabla P Y s) x - nabla P Y (nabla P X s) x -
40     nabla P (VectorField.lieBracket ℝ X Y) s x
41 
42 /-- The operator-valued two-form coefficient P[dP(v),dP(w)]P. -/
43 noncomputable def curvatureForm (P : E → F →L[ℝ] F) (x v w : E) : F →L[ℝ] F :=
44   P x * (fderiv ℝ P x v * fderiv ℝ P x w -
45     fderiv ℝ P x w * fderiv ℝ P x v) * P x
46 
47 theorem nabla_in_range (P : E → F →L[ℝ] F)
48     (hP : ∀ x, P x * P x = P x) (X : E → E) (s : E → F) (x : E) :
49     P x (nabla P X s x) = nabla P X s x := by
50   exact congrArg (fun L : F →L[ℝ] F => L (fderiv ℝ s x (X x))) (hP x)
51 
52 theorem projector_jet (P : E → F →L[ℝ] F) (hP : Differentiable ℝ P)
53     (hPP : ∀ x, P x * P x = P x) (x v : E) :
54     fderiv ℝ P x v * P x + P x * fderiv ℝ P x v = fderiv ℝ P x v := by
55   have heq : (fun y => P y * P y) = P := funext hPP
56   have hh := congrArg (fun L => L v) (fderiv_fun_mul' (hP x) (hP x))
57   rw [heq] at hh
58   simpa [add_comm] using hh.symm
59 
60 theorem projector_differential_sandwich (P : E → F →L[ℝ] F)
61     (hP : Differentiable ℝ P) (hPP : ∀ x, P x * P x = P x) (x v : E) :
62     P x * fderiv ℝ P x v * P x = 0 :=
63   jet_sandwich_zero _ _ (hPP x) (projector_jet P hP hPP x v)
64 
65 theorem section_jet (P : E → F →L[ℝ] F) (s : E → F)
66     (hP : Differentiable ℝ P) (hs : Differentiable ℝ s)
67     (hPs : ∀ x, P x (s x) = s x) (x v : E) :
68     fderiv ℝ s x v = fderiv ℝ P x v (s x) + P x (fderiv ℝ s x v) := by
69   have heq : (fun y => P y (s y)) = s := funext hPs
70   have hh := congrArg (fun L => L v) (fderiv_clm_apply (hP x) (hs x))
71   rw [heq] at hh
72   simpa [add_comm] using hh
73 
74 theorem nabla_derivative (P : E → F →L[ℝ] F) (Y : E → E) (s : E → F)
75     (hP : Differentiable ℝ P) (hY : Differentiable ℝ Y)
76     (hs : ContDiff ℝ 2 s) (x v : E) :
77     fderiv ℝ (nabla P Y s) x v =
78       P x (fderiv ℝ (fun y => fderiv ℝ s y (Y y)) x v) +
79       fderiv ℝ P x v (fderiv ℝ s x (Y x)) := by
80   have hs' : Differentiable ℝ (fderiv ℝ s) :=
81     ((contDiff_succ_iff_fderiv (n := 1)).mp hs).2.2.differentiable_one
82   have hh := congrArg (fun L => L v)
83     (fderiv_clm_apply (hP x) ((hs' x).clm_apply (hY x)))
84   change (fderiv ℝ (fun y => P y (fderiv ℝ s y (Y y))) x) v = _
85   simpa using hh
86 
87 theorem curvature_expansion (P : E → F →L[ℝ] F) (X Y : E → E) (s : E → F)
88     (hP : Differentiable ℝ P) (hPP : ∀ x, P x * P x = P x)
89     (hX : Differentiable ℝ X) (hY : Differentiable ℝ Y)
90     (hs : ContDiff ℝ 2 s) (x : E) :
91     curvature P X Y s x =
92       P x (fderiv ℝ P x (X x) (fderiv ℝ s x (Y x))) -
93       P x (fderiv ℝ P x (Y x) (fderiv ℝ s x (X x))) := by
94   have hp (z : F) : P x (P x z) = P x z :=
95     congrArg (fun L : F →L[ℝ] F => L z) (hPP x)
96   have hb := VectorField.fderiv_apply_lieBracket (hs.contDiffAt (x := x))
97     (by simp : minSmoothness ℝ 2 ≤ (2 : ℕ∞ω)) (hY x) (hX x)
98   unfold curvature
99   simp only [nabla]
100   rw [nabla_derivative P Y s hP hY hs x (X x),
101     nabla_derivative P X s hP hX hs x (Y x)]
102   simp only [map_add, hp, hb, map_sub]
103   abel
104 
105 /-- Full chart-level curvature formula for actual vector-valued range sections. -/
106 theorem projected_connection_curvature (P : E → F →L[ℝ] F)
107     (X Y : E → E) (s : E → F)
108     (hP : Differentiable ℝ P) (hPP : ∀ x, P x * P x = P x)
109     (hX : Differentiable ℝ X) (hY : Differentiable ℝ Y)
110     (hs : ContDiff ℝ 2 s) (hPs : ∀ x, P x (s x)=s x) (x : E) :
111     curvature P X Y s x = curvatureForm P x (X x) (Y x) (s x) := by
112   have hs1 : Differentiable ℝ s := hs.differentiable (by norm_num)
113   have hz (v : E) (z : F) : P x (fderiv ℝ P x v (P x z)) = 0 := by
114     have hh := congrArg (fun L : F →L[ℝ] F => L z)
115       (projector_differential_sandwich P hP hPP x v)
116     simpa [mul_apply_eq_comp] using hh
117   rw [curvature_expansion P X Y s hP hPP hX hY hs x]
118   conv_lhs => rw [section_jet P s hP hs1 hPs x (Y x),
119     section_jet P s hP hs1 hPs x (X x)]
120   simp only [map_add, hz, add_zero]
121   simp [curvatureForm, hPs, map_sub]
122 
123 theorem curvatureForm_alternating (P : E → F →L[ℝ] F) (x v : E) :
124     curvatureForm P x v v = 0 := by simp [curvatureForm]
125 
126 theorem curvatureForm_antisymmetric (P : E → F →L[ℝ] F) (x v w : E) :
127     curvatureForm P x v w = -curvatureForm P x w v := by
128   unfold curvatureForm
129   noncomm_ring
130 
131 theorem curvatureForm_left_range (P : E → F →L[ℝ] F)
132     (hPP : ∀ x, P x*P x=P x) (x v w : E) :
133     P x * curvatureForm P x v w = curvatureForm P x v w := by
134   simp only [curvatureForm, ← mul_assoc, hPP]
135 
136 theorem curvatureForm_right_range (P : E → F →L[ℝ] F)
137     (hPP : ∀ x, P x*P x=P x) (x v w : E) :
138     curvatureForm P x v w * P x = curvatureForm P x v w := by
139   simp only [curvatureForm, mul_assoc, hPP]
140 
141 /-- The two-form coefficients transform by the actual chain rule. -/
142 theorem curvatureForm_pullback {D : Type*} [NormedAddCommGroup D] [NormedSpace ℝ D]
143     (f : D → E) (P : E → F →L[ℝ] F) (x v w : D)
144     (hf : DifferentiableAt ℝ f x) (hP : DifferentiableAt ℝ P (f x)) :
145     curvatureForm (P ∘ f) x v w =
146       curvatureForm P (f x) (fderiv ℝ f x v) (fderiv ℝ f x w) := by
147   simp [curvatureForm, fderiv_comp x hP hf]
148 /-- Connection Leibniz rule on actual range sections. -/
149 theorem nabla_scalar_leibniz (P : E → F →L[ℝ] F) (X : E → E)
150     (s : E → F) (c : E → ℝ) (x : E)
151     (hs : DifferentiableAt ℝ s x) (hc : DifferentiableAt ℝ c x)
152     (hPs : P x (s x)=s x) :
153     nabla P X (fun y => c y • s y) x =
154       (fderiv ℝ c x (X x)) • s x + c x • nabla P X s x := by
155   simp [nabla, fderiv_fun_smul hc hs, hPs, add_comm]
156 
157 theorem nabla_add_vectorfields (P : E → F →L[ℝ] F) (X Y : E → E)
158     (s : E → F) (x : E) :
159     nabla P (fun y => X y+Y y) s x = nabla P X s x+nabla P Y s x := by
160   simp [nabla]
161 
162 theorem nabla_smul_vectorfield (P : E → F →L[ℝ] F) (X : E → E)
163     (s : E → F) (c : E → ℝ) (x : E) :
164     nabla P (fun y => c y • X y) s x = c x • nabla P X s x := by
165   simp [nabla]
166 
167 theorem curvatureForm_add_left (P : E → F →L[ℝ] F) (x u v w : E) :
168     curvatureForm P x (u+v) w = curvatureForm P x u w+curvatureForm P x v w := by
169   simp only [curvatureForm, map_add]
170   noncomm_ring
171 
172 theorem curvatureForm_add_right (P : E → F →L[ℝ] F) (x u v w : E) :
173     curvatureForm P x u (v+w) = curvatureForm P x u v+curvatureForm P x u w := by
174   simp only [curvatureForm, map_add]
175   noncomm_ring
176 
177 theorem curvatureForm_smul_left (P : E → F →L[ℝ] F) (x u v : E) (c : ℝ) :
178     curvatureForm P x (c • u) v = c • curvatureForm P x u v := by
179   simp only [curvatureForm, map_smul, smul_mul_assoc, mul_smul_comm, ← smul_sub]
180 
181 theorem curvatureForm_smul_right (P : E → F →L[ℝ] F) (x u v : E) (c : ℝ) :
182     curvatureForm P x u (c • v) = c • curvatureForm P x u v := by
183   simp only [curvatureForm, map_smul, smul_mul_assoc, mul_smul_comm, ← smul_sub]
184 
185 end KomorebiPaperVII.Curvature
186 
187 /-! Complete declaration-level trust audit. -/
188 #print axioms KomorebiPaperVII.Curvature.jet_sandwich_zero
189 #print axioms KomorebiPaperVII.Curvature.nabla_in_range
190 #print axioms KomorebiPaperVII.Curvature.projector_jet
191 #print axioms KomorebiPaperVII.Curvature.projector_differential_sandwich
192 #print axioms KomorebiPaperVII.Curvature.section_jet
193 #print axioms KomorebiPaperVII.Curvature.nabla_derivative
194 #print axioms KomorebiPaperVII.Curvature.curvature_expansion
195 #print axioms KomorebiPaperVII.Curvature.projected_connection_curvature
196 #print axioms KomorebiPaperVII.Curvature.curvatureForm_alternating
197 #print axioms KomorebiPaperVII.Curvature.curvatureForm_antisymmetric
198 #print axioms KomorebiPaperVII.Curvature.curvatureForm_left_range
199 #print axioms KomorebiPaperVII.Curvature.curvatureForm_right_range
200 #print axioms KomorebiPaperVII.Curvature.curvatureForm_pullback
201 #print axioms KomorebiPaperVII.Curvature.nabla_scalar_leibniz
202 #print axioms KomorebiPaperVII.Curvature.nabla_add_vectorfields
203 #print axioms KomorebiPaperVII.Curvature.nabla_smul_vectorfield
204 #print axioms KomorebiPaperVII.Curvature.curvatureForm_add_left
205 #print axioms KomorebiPaperVII.Curvature.curvatureForm_add_right
206 #print axioms KomorebiPaperVII.Curvature.curvatureForm_smul_left
207 #print axioms KomorebiPaperVII.Curvature.curvatureForm_smul_right

Back to source controls