LocalProjectedCurvature.lean

1 module
2 public import ProjectedCurvature
3 import all ProjectedCurvature
4 public import Mathlib.Analysis.Calculus.VectorField
5 public import Mathlib.Analysis.Calculus.FDeriv.Mul
6 public import Mathlib.Analysis.Calculus.FDeriv.CompCLM
7 public import Mathlib.Analysis.Normed.Operator.Mul
8 public import Mathlib.Tactic
9 /-! Author: Komorebi P. Paper VII, sixth block.
10 Actual Frechet derivatives and actual vector fields, including the Lie bracket.
11 Point-local hypotheses allow application inside arbitrary open chart domains.
12 The manifold construction imports these results. -/
13 public section
14 set_option autoImplicit false
15 set_option backward.isDefEq.respectTransparency false
16 set_option backward.isDefEq.respectTransparency.types false
17 set_option linter.unusedSectionVars false
18 namespace KomorebiPaperVII.LocalCurvature
19 open KomorebiPaperVII.Curvature
20 open scoped ContDiff
21 
22 variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
23   [NormedAddCommGroup F] [NormedSpace ℝ F]
24 
25 theorem projector_jet (P : E → F →L[ℝ] F) (x : E) (hP : DifferentiableAt ℝ P x)
26     (hPP : ∀ x, P x * P x = P x) (v : E) :
27     fderiv ℝ P x v * P x + P x * fderiv ℝ P x v = fderiv ℝ P x v := by
28   have heq : (fun y => P y * P y) = P := funext hPP
29   have hh := congrArg (fun L => L v) (fderiv_fun_mul' hP hP)
30   rw [heq] at hh
31   simpa [add_comm] using hh.symm
32 
33 theorem projector_differential_sandwich (P : E → F →L[ℝ] F)
34     (x : E) (hP : DifferentiableAt ℝ P x) (hPP : ∀ x, P x * P x = P x) (v : E) :
35     P x * fderiv ℝ P x v * P x = 0 :=
36   jet_sandwich_zero _ _ (hPP x) (projector_jet P x hP hPP v)
37 
38 theorem section_jet (P : E → F →L[ℝ] F) (s : E → F) (x : E)
39     (hP : DifferentiableAt ℝ P x) (hs : DifferentiableAt ℝ s x)
40     (hPs : ∀ x, P x (s x) = s x) (v : E) :
41     fderiv ℝ s x v = fderiv ℝ P x v (s x) + P x (fderiv ℝ s x v) := by
42   have heq : (fun y => P y (s y)) = s := funext hPs
43   have hh := congrArg (fun L => L v) (fderiv_clm_apply hP hs)
44   rw [heq] at hh
45   simpa [add_comm] using hh
46 
47 theorem nabla_derivative (P : E → F →L[ℝ] F) (Y : E → E) (s : E → F) (x : E)
48     (hP : DifferentiableAt ℝ P x) (hY : DifferentiableAt ℝ Y x)
49     (hs : ContDiffAt ℝ 2 s x) (v : E) :
50     fderiv ℝ (nabla P Y s) x v =
51       P x (fderiv ℝ (fun y => fderiv ℝ s y (Y y)) x v) +
52       fderiv ℝ P x v (fderiv ℝ s x (Y x)) := by
53   have hs' : DifferentiableAt ℝ (fderiv ℝ s) x :=
54     (hs.fderiv_right (m := 1) (by norm_num)).differentiableAt one_ne_zero
55   have hh := congrArg (fun L => L v)
56     (fderiv_clm_apply hP (hs'.clm_apply hY))
57   change (fderiv ℝ (fun y => P y (fderiv ℝ s y (Y y))) x) v = _
58   simpa using hh
59 
60 theorem curvature_expansion (P : E → F →L[ℝ] F) (X Y : E → E) (s : E → F) (x : E)
61     (hP : DifferentiableAt ℝ P x) (hPP : ∀ x, P x * P x = P x)
62     (hX : DifferentiableAt ℝ X x) (hY : DifferentiableAt ℝ Y x)
63     (hs : ContDiffAt ℝ 2 s x) :
64     curvature P X Y s x =
65       P x (fderiv ℝ P x (X x) (fderiv ℝ s x (Y x))) -
66       P x (fderiv ℝ P x (Y x) (fderiv ℝ s x (X x))) := by
67   have hp (z : F) : P x (P x z) = P x z :=
68     congrArg (fun L : F →L[ℝ] F => L z) (hPP x)
69   have hb := VectorField.fderiv_apply_lieBracket hs
70     (by simp : minSmoothness ℝ 2 ≤ (2 : ℕ∞ω)) hY hX
71   unfold curvature
72   simp only [nabla]
73   rw [nabla_derivative P Y s x hP hY hs (X x),
74     nabla_derivative P X s x hP hX hs (Y x)]
75   simp only [map_add, hp, hb, map_sub]
76   abel
77 
78 /-- Full chart-level curvature formula for actual vector-valued range sections. -/
79 theorem projected_connection_curvature (P : E → F →L[ℝ] F)
80     (X Y : E → E) (s : E → F) (x : E)
81     (hP : DifferentiableAt ℝ P x) (hPP : ∀ x, P x * P x = P x)
82     (hX : DifferentiableAt ℝ X x) (hY : DifferentiableAt ℝ Y x)
83     (hs : ContDiffAt ℝ 2 s x) (hPs : ∀ x, P x (s x)=s x) :
84     curvature P X Y s x = curvatureForm P x (X x) (Y x) (s x) := by
85   have hs1 : DifferentiableAt ℝ s x := hs.differentiableAt (by norm_num)
86   have hz (v : E) (z : F) : P x (fderiv ℝ P x v (P x z)) = 0 := by
87     have hh := congrArg (fun L : F →L[ℝ] F => L z)
88       (projector_differential_sandwich P x hP hPP v)
89     simpa [mul_apply_eq_comp] using hh
90   rw [curvature_expansion P X Y s x hP hPP hX hY hs]
91   conv_lhs => rw [section_jet P s x hP hs1 hPs (Y x),
92     section_jet P s x hP hs1 hPs (X x)]
93   simp only [map_add, hz, add_zero]
94   simp [curvatureForm, hPs, map_sub]
95 
96 
97 end KomorebiPaperVII.LocalCurvature
98 
99 /-! Declaration-level dependency audit. -/
100 #print axioms KomorebiPaperVII.LocalCurvature.projector_jet
101 #print axioms KomorebiPaperVII.LocalCurvature.projector_differential_sandwich
102 #print axioms KomorebiPaperVII.LocalCurvature.section_jet
103 #print axioms KomorebiPaperVII.LocalCurvature.nabla_derivative
104 #print axioms KomorebiPaperVII.LocalCurvature.curvature_expansion
105 #print axioms KomorebiPaperVII.LocalCurvature.projected_connection_curvature

Back to source controls