Skip to content

Commit 565c61d

Browse files
Xinze-Li-MoqianXinze-Li-Moqian
committed
Curvature/Tensoriality: Z-slot Leibniz for riemannCurvature
R(X, Y)(f · Z)(x) = f(x) · R(X, Y) Z(x) for smooth scalar f and smooth vector fields X, Y, Z. Proof structure (textbook): - Inner Leibniz on ∇_V (f Z) = f · ∇_V Z + V(f) · Z (covDeriv_smul_field pointwise + funext). - Outer additivity (covDeriv_add_field) split into 2 sub-derivatives. - Outer Leibniz (covDeriv_smul_field × 4) on each sub-derivative. - Third term ∇_{[X,Y]} (f Z) x via direct covDeriv_smul_field. - Hessian-Lie identity X(Yf) - Y(Xf) = mfderiv f ([X, Y]) cancels the cross-derivative residual (Z-coefficient becomes 0). - AddCommGroup arithmetic (abel + smul_sub) closes. Auxiliary lemma mfderiv_apply_smoothVF_contMDiff: y ↦ mfderiv f y (V y) is C∞ when f, V are C∞. Routes through gradient duality manifoldGradient_inner_eq + metricInner smoothness (HasMetric.metricInner_contMDiffAt). This is the OpenGALib analog of external riemannSec_smul_third (differential-geometry/.../Curvature.lean:521). Cornerstone of the full 3-slot tensoriality bridge needed by the heart-of-Bochner outer assembly.
1 parent 3487e1a commit 565c61d

1 file changed

Lines changed: 201 additions & 0 deletions

File tree

‎OpenGALib/Riemannian/Curvature/Tensoriality.lean‎

Lines changed: 201 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,201 @@
1+
import OpenGALib.Riemannian.Curvature
2+
import OpenGALib.Riemannian.Gradient
3+
4+
/-!
5+
# Tensoriality of the Riemann curvature tensor — Z-slot Leibniz
6+
7+
`R(X, Y)(f · Z)(x) = f(x) · R(X, Y) Z(x)` for smooth scalar `f` and smooth
8+
vector fields `X, Y, Z`. The cross-derivative residual cancels by the
9+
manifold scalar Hessian-Lie identity.
10+
11+
This is the cornerstone of full 3-slot tensoriality (used by the
12+
heart-of-Bochner outer assembly). -/
13+
14+
noncomputable section
15+
16+
set_option linter.unusedSectionVars false
17+
18+
open Bundle VectorField
19+
open scoped ContDiff Manifold Bundle Riemannian Topology
20+
21+
namespace Riemannian
22+
23+
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
24+
[FiniteDimensional ℝ E]
25+
{H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
26+
{M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
27+
[IsLocallyConstantChartedSpace H M]
28+
[hm : HasMetric I M]
29+
30+
/-- **Smoothness of `y ↦ mfderiv f y (V y)` as a scalar function** for
31+
smooth scalar `f` and smooth tangent section `V`. The directional
32+
derivative `V(f)` is C∞.
33+
34+
OpenGALib analog of external `extDerivFun_apply_contMDiff`. Proof routes
35+
through the manifold-gradient duality `mfderiv f y v = ⟨∇^M f, v⟩_g`,
36+
which is `metricInner ∘ manifoldGradient ∘ ·`, smooth as a composition. -/
37+
theorem mfderiv_apply_smoothVF_contMDiff
38+
(f : M → ℝ) (V : SmoothVectorField I M)
39+
(hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) :
40+
ContMDiff I 𝓘(ℝ, ℝ) ∞
41+
(fun y => (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f y (V.toFun y))) := by
42+
-- Identify with `y ↦ metricInner y (manifoldGradient f y) (V y)` via grad duality.
43+
-- Then smoothness follows from manifoldGradient smoothness + V smoothness +
44+
-- bilinearity of the metric (encoded in `HasMetric` smoothness).
45+
have h_eq : (fun y => (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f y (V.toFun y)))
46+
= (fun y => metricInner y (manifoldGradient (I := I) f y) (V.toFun y)) := by
47+
funext y
48+
exact (manifoldGradient_inner_eq (I := I) f y (V.toFun y)).symm
49+
rw [h_eq]
50+
exact fun y => hm.metric.metricInner_contMDiffAt
51+
(n := ∞) (manifoldGradient_smooth_of_smooth (I := I) f hf y) (V.smooth y)
52+
53+
/-- **3rd-slot (Z-slot) C∞-linearity of `riemannCurvature`**:
54+
$$R(X, Y)(f \cdot Z)(x) = f(x) \cdot R(X, Y)\,Z(x).$$
55+
56+
External reference: `riemannSec_smul_third` in
57+
`differential-geometry/.../Curvature.lean:521`. -/
58+
theorem riemannCurvature_smul_third_field
59+
[IsManifold I 2 M]
60+
(f : M → ℝ) (X Y Z : SmoothVectorField I M) (x : M)
61+
(h_interior : extChartAt I x x ∈ closure (interior (Set.range I)))
62+
(hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) :
63+
riemannCurvature X.toFun Y.toFun (f • Z.toFun) x
64+
= f x • riemannCurvature X.toFun Y.toFun Z.toFun x := by
65+
classical
66+
have hf_at : ∀ y, MDifferentiableAt I 𝓘(ℝ, ℝ) f y :=
67+
fun y => (hf y).mdifferentiableAt (by simp)
68+
have hf_C2_at : ContMDiffAt I 𝓘(ℝ, ℝ) 2 f x :=
69+
(hf x).of_le (by
70+
show ((2 : ℕ∞) : ℕ∞ω) ≤ ∞
71+
exact_mod_cast (le_top : (2 : ℕ∞) ≤ ⊤))
72+
have hX1 : ContMDiffAt I (I.prod 𝓘(ℝ, E)) 1
73+
(fun y => (⟨y, X.toFun y⟩ : TangentBundle I M)) x :=
74+
(X.smooth x).of_le (by
75+
show ((1 : ℕ∞) : ℕ∞ω) ≤ ∞
76+
exact_mod_cast (le_top : (1 : ℕ∞) ≤ ⊤))
77+
have hY1 : ContMDiffAt I (I.prod 𝓘(ℝ, E)) 1
78+
(fun y => (⟨y, Y.toFun y⟩ : TangentBundle I M)) x :=
79+
(Y.smooth x).of_le (by
80+
show ((1 : ℕ∞) : ℕ∞ω) ≤ ∞
81+
exact_mod_cast (le_top : (1 : ℕ∞) ≤ ⊤))
82+
-- Directional-derivative scalar functions.
83+
set Yf : M → ℝ :=
84+
fun y => (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f y (Y.toFun y)) with hYf_def
85+
set Xf : M → ℝ :=
86+
fun y => (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f y (X.toFun y)) with hXf_def
87+
-- Smoothness of Yf, Xf as C∞ scalar functions.
88+
have hYf_smooth : ContMDiff I 𝓘(ℝ, ℝ) ∞ Yf :=
89+
mfderiv_apply_smoothVF_contMDiff (I := I) f Y hf
90+
have hXf_smooth : ContMDiff I 𝓘(ℝ, ℝ) ∞ Xf :=
91+
mfderiv_apply_smoothVF_contMDiff (I := I) f X hf
92+
have hYf_at : MDifferentiableAt I 𝓘(ℝ, ℝ) Yf x :=
93+
(hYf_smooth x).mdifferentiableAt (by simp)
94+
have hXf_at : MDifferentiableAt I 𝓘(ℝ, ℝ) Xf x :=
95+
(hXf_smooth x).mdifferentiableAt (by simp)
96+
-- ∇_V (f Z) section identity at every y (V ∈ {X, Y}).
97+
-- We state as Π-pointwise functions (not lambda-form) to match `covDeriv` shape.
98+
have h_inner_Y :
99+
covDeriv Y.toFun (f • Z.toFun)
100+
= (fun y : M => f y • covDeriv Y.toFun Z.toFun y + Yf y • Z.toFun y) := by
101+
funext y
102+
exact covDeriv_smul_field Y.toFun f Z.toFun y (hf_at y) (Z.smoothAt y)
103+
have h_inner_X :
104+
covDeriv X.toFun (f • Z.toFun)
105+
= (fun y : M => f y • covDeriv X.toFun Z.toFun y + Xf y • Z.toFun y) := by
106+
funext y
107+
exact covDeriv_smul_field X.toFun f Z.toFun y (hf_at y) (Z.smoothAt y)
108+
-- Riemann curvature unfold via def.
109+
rw [riemannCurvature_def, riemannCurvature_def, h_inner_Y, h_inner_X]
110+
-- Pointwise sums need to be split into Π-add form for `covDeriv_add_field`.
111+
-- The two summands as separate Π-sections.
112+
set g1Y : Π y : M, TangentSpace I y :=
113+
fun y => f y • covDeriv Y.toFun Z.toFun y with hg1Y_def
114+
set g2Y : Π y : M, TangentSpace I y :=
115+
fun y => Yf y • Z.toFun y with hg2Y_def
116+
set g1X : Π y : M, TangentSpace I y :=
117+
fun y => f y • covDeriv X.toFun Z.toFun y with hg1X_def
118+
set g2X : Π y : M, TangentSpace I y :=
119+
fun y => Xf y • Z.toFun y with hg2X_def
120+
-- Convert `fun y => g1Y y + g2Y y` to Π-add `g1Y + g2Y` definitionally.
121+
have h_pi_addY : (fun y : M => g1Y y + g2Y y) = g1Y + g2Y := rfl
122+
have h_pi_addX : (fun y : M => g1X y + g2X y) = g1X + g2X := rfl
123+
rw [h_pi_addY, h_pi_addX]
124+
-- Smoothness witnesses for the summands at x.
125+
have h_dY_Z_smooth : TangentSmoothAt (fun y => covDeriv Y.toFun Z.toFun y) x :=
126+
covDeriv_smoothVF_smoothAt Y Z x
127+
have h_dX_Z_smooth : TangentSmoothAt (fun y => covDeriv X.toFun Z.toFun y) x :=
128+
covDeriv_smoothVF_smoothAt X Z x
129+
have hg1Y_smooth : TangentSmoothAt g1Y x :=
130+
(hf_at x).smul_section h_dY_Z_smooth
131+
have hg2Y_smooth : TangentSmoothAt g2Y x :=
132+
hYf_at.smul_section (Z.smoothAt x)
133+
have hg1X_smooth : TangentSmoothAt g1X x :=
134+
(hf_at x).smul_section h_dX_Z_smooth
135+
have hg2X_smooth : TangentSmoothAt g2X x :=
136+
hXf_at.smul_section (Z.smoothAt x)
137+
-- Apply outer additivity (covDeriv_add_field).
138+
rw [covDeriv_add_field X.toFun g1Y g2Y x hg1Y_smooth hg2Y_smooth,
139+
covDeriv_add_field Y.toFun g1X g2X x hg1X_smooth hg2X_smooth]
140+
-- Apply Leibniz to each summand at x.
141+
-- g1Y = f • (∇_Y Z), g2Y = Yf • Z, g1X = f • (∇_X Z), g2X = Xf • Z.
142+
-- ∇_X (f • ∇_Y Z) x = f x • ∇_X (∇_Y Z) x + (Xf x) • (∇_Y Z) x.
143+
have hT1_g1Y : covDeriv X.toFun g1Y x
144+
= f x • covDeriv X.toFun (fun y => covDeriv Y.toFun Z.toFun y) x
145+
+ (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f x (X.toFun x))
146+
• covDeriv Y.toFun Z.toFun x :=
147+
covDeriv_smul_field X.toFun f
148+
(fun y => covDeriv Y.toFun Z.toFun y) x (hf_at x) h_dY_Z_smooth
149+
have hT1_g2Y : covDeriv X.toFun g2Y x
150+
= Yf x • covDeriv X.toFun Z.toFun x
151+
+ (show ℝ from mfderiv I 𝓘(ℝ, ℝ) Yf x (X.toFun x)) • Z.toFun x :=
152+
covDeriv_smul_field X.toFun Yf Z.toFun x hYf_at (Z.smoothAt x)
153+
have hT2_g1X : covDeriv Y.toFun g1X x
154+
= f x • covDeriv Y.toFun (fun y => covDeriv X.toFun Z.toFun y) x
155+
+ (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f x (Y.toFun x))
156+
• covDeriv X.toFun Z.toFun x :=
157+
covDeriv_smul_field Y.toFun f
158+
(fun y => covDeriv X.toFun Z.toFun y) x (hf_at x) h_dX_Z_smooth
159+
have hT2_g2X : covDeriv Y.toFun g2X x
160+
= Xf x • covDeriv Y.toFun Z.toFun x
161+
+ (show ℝ from mfderiv I 𝓘(ℝ, ℝ) Xf x (Y.toFun x)) • Z.toFun x :=
162+
covDeriv_smul_field Y.toFun Xf Z.toFun x hXf_at (Z.smoothAt x)
163+
-- Third term: ∇_{[X,Y]} (f Z) x = f x • ∇_{[X,Y]} Z x + (mfderiv f x ([X,Y] x)) • Z x.
164+
have hT3 : covDeriv (mlieBracket I X.toFun Y.toFun) (f • Z.toFun) x
165+
= f x • covDeriv (mlieBracket I X.toFun Y.toFun) Z.toFun x
166+
+ (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f x
167+
(mlieBracket I X.toFun Y.toFun x)) • Z.toFun x :=
168+
covDeriv_smul_field (mlieBracket I X.toFun Y.toFun) f Z.toFun x
169+
(hf_at x) (Z.smoothAt x)
170+
rw [hT1_g1Y, hT1_g2Y, hT2_g1X, hT2_g2X, hT3]
171+
-- Apply Hessian-Lie identity: X(Yf) x - Y(Xf) x = mfderiv f x ([X,Y] x).
172+
have h_HL : (show ℝ from mfderiv I 𝓘(ℝ, ℝ) Yf x (X.toFun x))
173+
- (show ℝ from mfderiv I 𝓘(ℝ, ℝ) Xf x (Y.toFun x))
174+
= (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f x
175+
(mlieBracket I X.toFun Y.toFun x)) :=
176+
mfderiv_iterate_sub_eq_mlieBracket_apply
177+
f X.toFun Y.toFun x h_interior hf_C2_at hX1 hY1
178+
-- Rewrite the `mfderiv f x ([X,Y] x) • Z x` term using h_HL to make
179+
-- the `(Yf' x - Xf' x) • Z x` cancellation explicit.
180+
rw [← h_HL, sub_smul]
181+
-- Identify `Xf x = mfderiv f x (X x)` and `Yf x = mfderiv f x (Y x)` definitionally
182+
-- (both sides reduce by `set ... with` unfolding).
183+
show f x • covDeriv X.toFun (fun y => covDeriv Y.toFun Z.toFun y) x
184+
+ Xf x • covDeriv Y.toFun Z.toFun x
185+
+ (Yf x • covDeriv X.toFun Z.toFun x
186+
+ (show ℝ from mfderiv I 𝓘(ℝ, ℝ) Yf x (X.toFun x)) • Z.toFun x)
187+
- (f x • covDeriv Y.toFun (fun y => covDeriv X.toFun Z.toFun y) x
188+
+ Yf x • covDeriv X.toFun Z.toFun x
189+
+ (Xf x • covDeriv Y.toFun Z.toFun x
190+
+ (show ℝ from mfderiv I 𝓘(ℝ, ℝ) Xf x (Y.toFun x)) • Z.toFun x))
191+
- (f x • covDeriv (mlieBracket I X.toFun Y.toFun) Z.toFun x
192+
+ ((show ℝ from mfderiv I 𝓘(ℝ, ℝ) Yf x (X.toFun x)) • Z.toFun x
193+
- (show ℝ from mfderiv I 𝓘(ℝ, ℝ) Xf x (Y.toFun x)) • Z.toFun x))
194+
= f x • (covDeriv X.toFun (fun y => covDeriv Y.toFun Z.toFun y) x
195+
- covDeriv Y.toFun (fun y => covDeriv X.toFun Z.toFun y) x
196+
- covDeriv (mlieBracket I X.toFun Y.toFun) Z.toFun x)
197+
-- Pure AddCommGroup arithmetic — cross-cancellation + f x • distributes.
198+
rw [smul_sub, smul_sub]
199+
abel
200+
201+
end Riemannian

0 commit comments

Comments
 (0)