diff --git a/OpenGALib/Riemannian/Connection/LeviCivita.lean b/OpenGALib/Riemannian/Connection/LeviCivita.lean index 08e2fc0..211e996 100644 --- a/OpenGALib/Riemannian/Connection/LeviCivita.lean +++ b/OpenGALib/Riemannian/Connection/LeviCivita.lean @@ -771,8 +771,11 @@ standard $C^2$ textbook setup but fire pointwise. **Ground truth**: do Carmo 1992 §4 Proposition 2.5 (ii). -/ theorem bianchi_first + (g : RiemannianMetric I M) (X Y Z : SmoothVectorField I M) (x : M) : - Riem(X, Y) Z x + Riem(Y, Z) X x + Riem(Z, X) Y x = 0 := by + riemannCurvature g X.toFun Y.toFun Z.toFun x + + riemannCurvature g Y.toFun Z.toFun X.toFun x + + riemannCurvature g Z.toFun X.toFun Y.toFun x = 0 := by -- Jacobi identity via the `SmoothVectorField.mlieBracket_jacobi` framework -- primitive (wraps Mathlib's `leibniz_identity_mlieBracket_apply`). have h_jac : (⟦X, ⟦Y, Z⟧⟧) x = (⟦⟦X, Y⟧, Z⟧) x + (⟦Y, ⟦X, Z⟧⟧) x := @@ -782,12 +785,12 @@ theorem bianchi_first have hX : ∀ y, TangentSmoothAt X.toFun y := X.smoothAt have hY : ∀ y, TangentSmoothAt Y.toFun y := Y.smoothAt have hZ : ∀ y, TangentSmoothAt Z.toFun y := Z.smoothAt - have h_dXZ : ∀ y, TangentSmoothAt ∇[X] Z y := - fun y => covDeriv_smoothVF_smoothAt HasMetric.metric X Z y - have h_dYX : ∀ y, TangentSmoothAt ∇[Y] X y := - fun y => covDeriv_smoothVF_smoothAt HasMetric.metric Y X y - have h_dZY : ∀ y, TangentSmoothAt ∇[Z] Y y := - fun y => covDeriv_smoothVF_smoothAt HasMetric.metric Z Y y + have h_dXZ : ∀ y, TangentSmoothAt (fun y => covDeriv g X.toFun Z.toFun y) y := + fun y => covDeriv_smoothVF_smoothAt g X Z y + have h_dYX : ∀ y, TangentSmoothAt (fun y => covDeriv g Y.toFun X.toFun y) y := + fun y => covDeriv_smoothVF_smoothAt g Y X y + have h_dZY : ∀ y, TangentSmoothAt (fun y => covDeriv g Z.toFun Y.toFun y) y := + fun y => covDeriv_smoothVF_smoothAt g Z Y y have h_XY : ∀ y, TangentSmoothAt ⟦X, Y⟧ y := fun _ => mlieBracket_tangentSmoothAt X.smooth Y.smooth have h_YX : ∀ y, TangentSmoothAt ⟦Y, X⟧ y := @@ -799,42 +802,45 @@ theorem bianchi_first have h_XZ : ∀ y, TangentSmoothAt ⟦X, Z⟧ y := fun _ => mlieBracket_tangentSmoothAt X.smooth Z.smooth -- Step 1: section-level torsion-freeness (Π-equalities, via global smoothness). - have eq_YZ : (∇[Y] Z : VectorFieldSection I M) = ∇[Z] Y + ⟦Y, Z⟧ := - covDeriv_section_eq_swap_add_mlieBracket HasMetric.metric Y Z hY hZ - have eq_ZX : (∇[Z] X : VectorFieldSection I M) = ∇[X] Z + ⟦Z, X⟧ := - covDeriv_section_eq_swap_add_mlieBracket HasMetric.metric Z X hZ hX - have eq_XY : (∇[X] Y : VectorFieldSection I M) = ∇[Y] X + ⟦X, Y⟧ := - covDeriv_section_eq_swap_add_mlieBracket HasMetric.metric X Y hX hY + have eq_YZ : ((fun y => covDeriv g Y.toFun Z.toFun y) : VectorFieldSection I M) + = (fun y => covDeriv g Z.toFun Y.toFun y) + ⟦Y, Z⟧ := + covDeriv_section_eq_swap_add_mlieBracket g Y.toFun Z.toFun hY hZ + have eq_ZX : ((fun y => covDeriv g Z.toFun X.toFun y) : VectorFieldSection I M) + = (fun y => covDeriv g X.toFun Z.toFun y) + ⟦Z, X⟧ := + covDeriv_section_eq_swap_add_mlieBracket g Z.toFun X.toFun hZ hX + have eq_XY : ((fun y => covDeriv g X.toFun Y.toFun y) : VectorFieldSection I M) + = (fun y => covDeriv g Y.toFun X.toFun y) + ⟦X, Y⟧ := + covDeriv_section_eq_swap_add_mlieBracket g X.toFun Y.toFun hX hY -- Step 2: unfold riemannCurvature, substitute section equalities, split via add_field. - show (∇[X] (∇[Y] Z)) x - - (∇[Y] (∇[X] Z)) x - - (∇[⟦X, Y⟧] Z) x - + ((∇[Y] (∇[Z] X)) x - - (∇[Z] (∇[Y] X)) x - - (∇[⟦Y, Z⟧] X) x) - + ((∇[Z] (∇[X] Y)) x - - (∇[X] (∇[Z] Y)) x - - (∇[⟦Z, X⟧] Y) x) = 0 + show (covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x + - covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x + - covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x) + + (covDeriv g Y.toFun (fun y => covDeriv g Z.toFun X.toFun y) x + - covDeriv g Z.toFun (fun y => covDeriv g Y.toFun X.toFun y) x + - covDeriv g (VectorField.mlieBracket I Y.toFun Z.toFun) X.toFun x) + + (covDeriv g Z.toFun (fun y => covDeriv g X.toFun Y.toFun y) x + - covDeriv g X.toFun (fun y => covDeriv g Z.toFun Y.toFun y) x + - covDeriv g (VectorField.mlieBracket I Z.toFun X.toFun) Y.toFun x) = 0 rw [eq_YZ, eq_ZX, eq_XY] - rw [covDeriv_add_field HasMetric.metric X ∇[Z] Y ⟦Y, Z⟧ x + rw [covDeriv_add_field g X.toFun (fun y => covDeriv g Z.toFun Y.toFun y) ⟦Y, Z⟧ x (h_dZY x) (h_YZ x), - covDeriv_add_field HasMetric.metric Y ∇[X] Z ⟦Z, X⟧ x + covDeriv_add_field g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) ⟦Z, X⟧ x (h_dXZ x) (h_ZX x), - covDeriv_add_field HasMetric.metric Z ∇[Y] X ⟦X, Y⟧ x + covDeriv_add_field g Z.toFun (fun y => covDeriv g Y.toFun X.toFun y) ⟦X, Y⟧ x (h_dYX x) (h_XY x)] -- Step 3: pointwise torsion-free pairings (∇_A B - ∇_B A = [A,B]): - have pair_X : (∇[X] ⟦Y, Z⟧) x - - (∇[⟦Y, Z⟧] X) x + have pair_X : covDeriv g X.toFun ⟦Y, Z⟧ x + - covDeriv g ⟦Y, Z⟧ X.toFun x = (⟦X, ⟦Y, Z⟧⟧) x := - covDeriv_sub_swap_eq_mlieBracket HasMetric.metric X ⟦Y, Z⟧ x (hX x) (h_YZ x) - have pair_Y : (∇[Y] ⟦Z, X⟧) x - - (∇[⟦Z, X⟧] Y) x + covDeriv_sub_swap_eq_mlieBracket g X.toFun ⟦Y, Z⟧ x (hX x) (h_YZ x) + have pair_Y : covDeriv g Y.toFun ⟦Z, X⟧ x + - covDeriv g ⟦Z, X⟧ Y.toFun x = (⟦Y, ⟦Z, X⟧⟧) x := - covDeriv_sub_swap_eq_mlieBracket HasMetric.metric Y ⟦Z, X⟧ x (hY x) (h_ZX x) - have pair_Z : (∇[Z] ⟦X, Y⟧) x - - (∇[⟦X, Y⟧] Z) x + covDeriv_sub_swap_eq_mlieBracket g Y.toFun ⟦Z, X⟧ x (hY x) (h_ZX x) + have pair_Z : covDeriv g Z.toFun ⟦X, Y⟧ x + - covDeriv g ⟦X, Y⟧ Z.toFun x = (⟦Z, ⟦X, Y⟧⟧) x := - covDeriv_sub_swap_eq_mlieBracket HasMetric.metric Z ⟦X, Y⟧ x (hZ x) (h_XY x) + covDeriv_sub_swap_eq_mlieBracket g Z.toFun ⟦X, Y⟧ x (hZ x) (h_XY x) -- Step 4: rearrange so abel collapses all 12 cov-terms via pair_X/Y/Z. -- The goal after rewrites is (with shorthand): -- (∇_X∇_Z Y + ∇_X[Y,Z]) - ∇_Y∇_X Z - ∇_{[X,Y]} Z @@ -845,17 +851,17 @@ theorem bianchi_first -- We rewrite using pair_X/Y/Z by isolating the LHS shapes. -- pair_X gives ∇_X[Y,Z] = pair_X.lhs.lhs ↦ … — to use pair_X as a substitution, -- we set up the equations as A = mlie + B and rewrite ∇_X[Y,Z] = mlie + ∇_{[Y,Z]} X: - have h_subX : (∇[X] ⟦Y, Z⟧) x + have h_subX : covDeriv g X.toFun ⟦Y, Z⟧ x = (⟦X, ⟦Y, Z⟧⟧) x - + (∇[⟦Y, Z⟧] X) x := by + + covDeriv g ⟦Y, Z⟧ X.toFun x := by rw [← pair_X]; abel - have h_subY : (∇[Y] ⟦Z, X⟧) x + have h_subY : covDeriv g Y.toFun ⟦Z, X⟧ x = (⟦Y, ⟦Z, X⟧⟧) x - + (∇[⟦Z, X⟧] Y) x := by + + covDeriv g ⟦Z, X⟧ Y.toFun x := by rw [← pair_Y]; abel - have h_subZ : (∇[Z] ⟦X, Y⟧) x + have h_subZ : covDeriv g Z.toFun ⟦X, Y⟧ x = (⟦Z, ⟦X, Y⟧⟧) x - + (∇[⟦X, Y⟧] Z) x := by + + covDeriv g ⟦X, Y⟧ Z.toFun x := by rw [← pair_Z]; abel rw [h_subX, h_subY, h_subZ] -- Goal now has 3 outer-bracket terms + 6 ∇_·_ terms; three pairs of ∇_{[·,·]} · diff --git a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean index 654a1b6..d2f601e 100644 --- a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean +++ b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean @@ -54,8 +54,9 @@ local notation "cF[" V "]" => SmoothVectorField.const (I := I) (M := M) V Reference: do Carmo §4 Proposition 2.5 (i). -/ theorem riemannCurvature_antisymm + (g : RiemannianMetric I M) (X Y Z : VectorFieldSection I M) (x : M) : - Riem(X, Y) Z x = -Riem(Y, X) Z x := by + riemannCurvature g X Y Z x = -riemannCurvature g Y X Z x := by simp only [riem_simp] rw [covDeriv_mlieBracket_swap_apply] abel @@ -239,35 +240,36 @@ Stated using `mDirDeriv` (the `ℝ`-typed `mfderiv` wrapper) on the LHS and `(leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun` (definitionally equal to `covDeriv HasMetric.metric`) on the RHS. -/ private lemma mDirDeriv_self_eq_two_metricInner_leviCivita_self + (g : RiemannianMetric I M) (V : VectorFieldSection I M) (Z : SmoothVectorField I M) (y : M) (hV : TangentSmoothAt V y) : - mDirDeriv (fun y' => metricInner y' (Z y') (Z y')) y (V y) - = 2 * metricInner y - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y (V y)) (Z y) := by + mDirDeriv (fun y' => g.metricInner y' (Z y') (Z y')) y (V y) + = 2 * g.metricInner y + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y (V y)) (Z y) := by -- Bridge metric-compat ∇ → `.toFun` form so `rw [hsym]` matches the structural shape. - have h := leviCivitaConnection_metric_compatible HasMetric.metric V Z.toFun Z.toFun y + have h := leviCivitaConnection_metric_compatible g V Z.toFun Z.toFun y hV (Z.smoothAt y) (Z.smoothAt y) simp only [← leviCivitaConnection_toFun_eq_covDeriv] at h -- Cast h to typeclass `metricInner` form for rw matching. - change mDirDeriv (fun y' => metricInner y' (Z y') (Z y')) y (V y) - = metricInner y - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y (V y)) + change mDirDeriv (fun y' => g.metricInner y' (Z y') (Z y')) y (V y) + = g.metricInner y + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y (V y)) (Z y) - + metricInner y (Z y) - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y (V y)) + + g.metricInner y (Z y) + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y (V y)) at h have hsym : - metricInner y (Z y) - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y (V y)) - = metricInner y - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y (V y)) (Z y) := - metricInner_comm y _ _ + g.metricInner y (Z y) + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y (V y)) + = g.metricInner y + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y (V y)) (Z y) := + g.metricInner_comm y _ _ rw [hsym] at h - have h_ℝ : mDirDeriv (fun y' => metricInner y' (Z y') (Z y')) y (V y) - = metricInner y - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y (V y)) (Z y) - + metricInner y - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y (V y)) (Z y) := + have h_ℝ : mDirDeriv (fun y' => g.metricInner y' (Z y') (Z y')) y (V y) + = g.metricInner y + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y (V y)) (Z y) + + g.metricInner y + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y (V y)) (Z y) := h rw [h_ℝ]; ring @@ -275,13 +277,14 @@ private lemma mDirDeriv_self_eq_two_metricInner_leviCivita_self $y \mapsto g(Z, Z)(y)$ along the smooth vector field $V$ equals $2\,g(\nabla_V Z, Z)(y)$. -/ private lemma fun_mDirDeriv_self_eq_two_metricInner_leviCivita_self + (g : RiemannianMetric I M) (V Z : SmoothVectorField I M) : - (fun y' : M => mDirDeriv (fun y'' => metricInner y'' (Z y'') (Z y'')) y' (V.toFun y')) - = (fun y' : M => 2 * metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + (fun y' : M => mDirDeriv (fun y'' => g.metricInner y'' (Z y'') (Z y'')) y' (V.toFun y')) + = (fun y' : M => 2 * g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) := by funext y' - exact mDirDeriv_self_eq_two_metricInner_leviCivita_self V.toFun Z y' (V.smoothAt y') + exact mDirDeriv_self_eq_two_metricInner_leviCivita_self g V.toFun Z y' (V.smoothAt y') /-- **Math.** **Iterated metric-compat identity at $x$**: differentiating the diagonal identity once more at $x$ in direction $W(x)$ and applying @@ -291,111 +294,112 @@ $$\tfrac12\,W\!\left(V (g(Z, Z))\right)(x) + \langle \nabla_V Z, \nabla_W Z\rangle_g(x).$$ -/ private lemma half_mDirDeriv_iterate_eq_metricInner_iterCovDeriv [IsManifold I 2 M] + (g : RiemannianMetric I M) (V W Z : SmoothVectorField I M) (x : M) : (1/2 : ℝ) * mDirDeriv (fun y' : M => mDirDeriv - (fun y'' => metricInner y'' (Z y'') (Z y'')) y' (V.toFun y')) x (W.toFun x) - = metricInner x - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (fun y' => covDeriv HasMetric.metric V.toFun Z.toFun y') x (W.toFun x)) + (fun y'' => g.metricInner y'' (Z y'') (Z y'')) y' (V.toFun y')) x (W.toFun x) + = g.metricInner x + ((leviCivitaConnection (I := I) (M := M) g).toFun + (fun y' => covDeriv g V.toFun Z.toFun y') x (W.toFun x)) (Z x) - + metricInner x (covDeriv HasMetric.metric V.toFun Z.toFun x) - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x (W.toFun x)) := by + + g.metricInner x (covDeriv g V.toFun Z.toFun x) + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x (W.toFun x)) := by -- Use function-equality form of the diagonal identity to rewrite the LHS -- inner function; then apply mfderiv_const_smul and metric-compat at x. - have h_fun := fun_mDirDeriv_self_eq_two_metricInner_leviCivita_self V Z + have h_fun := fun_mDirDeriv_self_eq_two_metricInner_leviCivita_self g V Z -- Sections smooth at x. - have hcovVZ : TangentSmoothAt (fun y' => covDeriv HasMetric.metric V.toFun Z.toFun y') x := - covDeriv_smoothVF_smoothAt HasMetric.metric V Z x + have hcovVZ : TangentSmoothAt (fun y' => covDeriv g V.toFun Z.toFun y') x := + covDeriv_smoothVF_smoothAt g V Z x -- The mfderiv of LHS (the iterated mDirDeriv expression) at x in dir W(x): -- by h_fun, equals mfderiv of `fun y' => 2 * g(∇_V Z, Z)(y')` at x in dir W(x). -- That = 2 * mfderiv (g(∇_V Z, Z)) x (W x), and by metric-compat at x: -- = 2 * [g(∇_W ∇_V Z, Z) + g(∇_V Z, ∇_W Z)] x. -- So (1/2) * LHS = g(∇_W ∇_V Z, Z) x + g(∇_V Z, ∇_W Z) x. - -- Bridge metric-compat ∇ → `.toFun` form for downstream `metricInner_comm` / `linarith`. - have h_compat := leviCivitaConnection_metric_compatible HasMetric.metric - W.toFun (fun y' => covDeriv HasMetric.metric V.toFun Z.toFun y') Z.toFun x + -- Bridge metric-compat ∇ → `.toFun` form for downstream `g.metricInner_comm` / `linarith`. + have h_compat := leviCivitaConnection_metric_compatible g + W.toFun (fun y' => covDeriv g V.toFun Z.toFun y') Z.toFun x (W.smoothAt x) hcovVZ (Z.smoothAt x) simp only [← leviCivitaConnection_toFun_eq_covDeriv] at h_compat -- h_compat : mfderiv (fun y' => g(∇_V Z, Z) y') x (W x) = -- g(∇_W (∇_V Z), Z) + g(∇_V Z, ∇_W Z) -- Rewrite the LHS function via h_fun: conv_lhs => rw [show (fun y' : M => mDirDeriv - (fun y'' => metricInner y'' (Z y'') (Z y'')) y' (V.toFun y')) - = (fun y' : M => 2 * metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + (fun y'' => g.metricInner y'' (Z y'') (Z y'')) y' (V.toFun y')) + = (fun y' : M => 2 * g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) from h_fun] -- Now LHS = (1/2) * mfderiv (fun y' => 2 * g(∇_V Z, Z) y') x (W x) -- Pull the 2 out: mfderiv (2 * h) x v = 2 * mfderiv h x v (linear). -- The function under mfderiv: fun y' => 2 * g(LC.toFun Z y' (V y'), Z y') -- equals 2 • (fun y' => g(LC.toFun Z y' (V y'), Z y')) via funext. -- Use mfderiv_const_smul; we need MDifferentiableAt of the inner section. - -- The "covDeriv HasMetric.metric V Z = LC.toFun Z y (V y)" is def-eq; the inner section's - -- smoothness at x is hcovVZ (via metricInner_mdifferentiableAt). + -- The "covDeriv g V Z = LC.toFun Z y (V y)" is def-eq; the inner section's + -- smoothness at x is hcovVZ (via g.metricInner_mdifferentiableAt). have h_inner_mdiff : MDifferentiableAt I 𝓘(ℝ, ℝ) - (fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + (fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) x := by - -- The function is `y' ↦ g(covDeriv HasMetric.metric V Z y', Z y')` (def-eq covDeriv HasMetric.metric ↔ LC.toFun). - -- Use `metricInner_mdifferentiableAt` with `hcovVZ` and `Z.smoothAt x`. - have h := hm.metric.metricInner_mdifferentiableAt - (v := fun y' => covDeriv HasMetric.metric V.toFun Z.toFun y') (w := Z.toFun) hcovVZ (Z.smoothAt x) + -- The function is `y' ↦ g(covDeriv g V Z y', Z y')` (def-eq covDeriv g ↔ LC.toFun). + -- Use `g.metricInner_mdifferentiableAt` with `hcovVZ` and `Z.smoothAt x`. + have h := g.metricInner_mdifferentiableAt + (v := fun y' => covDeriv g V.toFun Z.toFun y') (w := Z.toFun) hcovVZ (Z.smoothAt x) exact h -- Avoid continuous linear map-smul issues by writing `2 * h = h + h` and using `mfderiv_add`. - have h_two_add : (fun y' : M => (2 : ℝ) * metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + have h_two_add : (fun y' : M => (2 : ℝ) * g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) - = (fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + = (fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y') - + metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + + g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) := by funext y'; ring rw [h_two_add] -- Now: (1/2) * mDirDeriv (fun y' => h y' + h y') x (W x) where h := g(∇_V Z, Z) y'. -- Convert `fun y' => h y' + h y'` to the Pi-add form `h + h` (definitional). - have h_pi_add : (fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + have h_pi_add : (fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y') - + metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + + g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) - = (fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + = (fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) - + (fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + + (fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) := rfl rw [h_pi_add] -- `mfderiv (f + g) x v = mfderiv f x v + mfderiv g x v`. -- Compute the continuous linear map add via `mfderiv_add` then evaluate at `W.toFun x`. have h_clm_add : - mfderiv I 𝓘(ℝ, ℝ) ((fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + mfderiv I 𝓘(ℝ, ℝ) ((fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) - + (fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + + (fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y'))) x - = mfderiv I 𝓘(ℝ, ℝ) (fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + = mfderiv I 𝓘(ℝ, ℝ) (fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) x - + mfderiv I 𝓘(ℝ, ℝ) (fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + + mfderiv I 𝓘(ℝ, ℝ) (fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) x := mfderiv_add h_inner_mdiff h_inner_mdiff -- Apply both sides to (W.toFun x) and use continuous linear map-add evaluation. - have h_val_add : mDirDeriv ((fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + have h_val_add : mDirDeriv ((fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) - + (fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + + (fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y'))) x (W.toFun x) - = mDirDeriv (fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + = mDirDeriv (fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) x (W.toFun x) - + mDirDeriv (fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + + mDirDeriv (fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) x (W.toFun x) := by show mfderiv I 𝓘(ℝ, ℝ) _ x (W.toFun x) = _ rw [h_clm_add] @@ -403,15 +407,15 @@ private lemma half_mDirDeriv_iterate_eq_metricInner_iterCovDeriv rw [h_val_add] -- Now: (1/2) * (mDirDeriv h x v + mDirDeriv h x v) = h_compat have h_compat_ℝ : - mDirDeriv (fun y' : M => metricInner y' - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y' (V.toFun y')) + mDirDeriv (fun y' : M => g.metricInner y' + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y' (V.toFun y')) (Z y')) x (W.toFun x) - = metricInner x - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (fun y' => covDeriv HasMetric.metric V.toFun Z.toFun y') x (W.toFun x)) + = g.metricInner x + ((leviCivitaConnection (I := I) (M := M) g).toFun + (fun y' => covDeriv g V.toFun Z.toFun y') x (W.toFun x)) (Z x) - + metricInner x (covDeriv HasMetric.metric V.toFun Z.toFun x) - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x (W.toFun x)) := + + g.metricInner x (covDeriv g V.toFun Z.toFun x) + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x (W.toFun x)) := h_compat rw [h_compat_ℝ]; ring @@ -421,16 +425,17 @@ $X, Y, Z$, with $x$ in the closure of the interior of $\mathrm{range}\,I$ Reference: do Carmo §4 Proposition 2.5(iii). -/ theorem riemannCurvature_inner_self_zero + (g : RiemannianMetric I M) [IsManifold I 2 M] (X Y Z : SmoothVectorField I M) (x : M) (h_interior : extChartAt I x x ∈ closure (interior (Set.range I))) : - metricInner x (Riem(X.toFun, Y.toFun) Z.toFun x) (Z x) = 0 := by + g.metricInner x (riemannCurvature g X.toFun Y.toFun Z.toFun x) (Z x) = 0 := by classical -- Setup: f := g(Z, Z), the self-norm-squared scalar function. - set f : M → ℝ := fun y' => metricInner y' (Z y') (Z y') with hf_def + set f : M → ℝ := fun y' => g.metricInner y' (Z y') (Z y') with hf_def -- f is C∞ globally, hence C² at x. have hf_smooth : ContMDiff I 𝓘(ℝ, ℝ) ∞ f := fun y => - hm.metric.metricInner_contMDiffAt (n := ∞) (Z.smooth y) (Z.smooth y) + g.metricInner_contMDiffAt (n := ∞) (Z.smooth y) (Z.smooth y) have hf_2 : ContMDiffAt I 𝓘(ℝ, ℝ) 2 f x := (hf_smooth x).of_le (by show ((2 : ℕ∞) : ℕ∞ω) ≤ ∞ @@ -439,10 +444,10 @@ theorem riemannCurvature_inner_self_zero have hXY_br : TangentSmoothAt (mlieBracket I X.toFun Y.toFun) x := mlieBracket_tangentSmoothAt X.smooth Y.smooth -- Equations (A) and (B): iterated metric-compat at x. - have hA := half_mDirDeriv_iterate_eq_metricInner_iterCovDeriv X Y Z x -- (V=X, W=Y) - have hB := half_mDirDeriv_iterate_eq_metricInner_iterCovDeriv Y X Z x -- (V=Y, W=X) + have hA := half_mDirDeriv_iterate_eq_metricInner_iterCovDeriv g X Y Z x -- (V=X, W=Y) + have hB := half_mDirDeriv_iterate_eq_metricInner_iterCovDeriv g Y X Z x -- (V=Y, W=X) -- Equation (C): metric-compat at x for V = [X, Y]. - have hC := mDirDeriv_self_eq_two_metricInner_leviCivita_self + have hC := mDirDeriv_self_eq_two_metricInner_leviCivita_self g (mlieBracket I X.toFun Y.toFun) Z x hXY_br -- Hessian–Lie identity at x: X(Y(f))(x) - Y(X(f))(x) = mfderiv f x ([X,Y](x)) have hX1 : ContMDiffAt I (I.prod 𝓘(ℝ, E)) 1 @@ -460,33 +465,33 @@ theorem riemannCurvature_inner_self_zero = mDirDeriv f x (mlieBracket I X.toFun Y.toFun x) := mfderiv_iterate_sub_eq_mlieBracket_apply f X.toFun Y.toFun x h_interior hf_2 hX1 hY1 -- Inner product cross-cancel: g(∇_X Z, ∇_Y Z) = g(∇_Y Z, ∇_X Z). - have h_inner_comm : metricInner x (covDeriv HasMetric.metric X.toFun Z.toFun x) - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x (Y.toFun x)) - = metricInner x (covDeriv HasMetric.metric Y.toFun Z.toFun x) - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x (X.toFun x)) := by - show metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x (X.toFun x)) - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x (Y.toFun x)) - = metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x (Y.toFun x)) - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x (X.toFun x)) - exact metricInner_comm x _ _ - -- Expand R via riemannCurvature_commutator_form HasMetric.metric + metricInner_sub_left twice. - show metricInner x (riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x) (Z x) = 0 + have h_inner_comm : g.metricInner x (covDeriv g X.toFun Z.toFun x) + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x (Y.toFun x)) + = g.metricInner x (covDeriv g Y.toFun Z.toFun x) + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x (X.toFun x)) := by + show g.metricInner x ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x (X.toFun x)) + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x (Y.toFun x)) + = g.metricInner x ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x (Y.toFun x)) + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x (X.toFun x)) + exact g.metricInner_comm x _ _ + -- Expand R via riemannCurvature_commutator_form g + g.metricInner_sub_left twice. + show g.metricInner x (riemannCurvature g X.toFun Y.toFun Z.toFun x) (Z x) = 0 rw [riemannCurvature_commutator_form] -- Goal: g(∇_X ∇_Y Z - ∇_Y ∇_X Z - ∇_{[X,Y]} Z, Z) x = 0 - rw [show metricInner x (covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x - - covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x - - covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x) (Z x) - = metricInner x (covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x) (Z x) - - metricInner x (covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x) (Z x) - - metricInner x (covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x) (Z x) + rw [show g.metricInner x (covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x + - covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x + - covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x) (Z x) + = g.metricInner x (covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x) (Z x) + - g.metricInner x (covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x) (Z x) + - g.metricInner x (covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x) (Z x) from by - rw [show ((covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x - - covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x - - covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x : TangentSpace I x)) - = (covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x - - covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x) - - covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x from rfl, - metricInner_sub_left, metricInner_sub_left]] + rw [show ((covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x + - covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x + - covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x : TangentSpace I x)) + = (covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x + - covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x) + - covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x from rfl, + g.metricInner_sub_left, g.metricInner_sub_left]] -- Now: g(∇_X ∇_Y Z, Z) - g(∇_Y ∇_X Z, Z) - g(∇_{[X,Y]} Z, Z) = 0 -- From hB (V=Y, W=X): (1/2) X(Y(f))(x) = g(∇_X ∇_Y Z, Z) + g(∇_Y Z, ∇_X Z) -- ⇒ g(∇_X ∇_Y Z, Z) = (1/2) X(Y(f))(x) - g(∇_Y Z, ∇_X Z) @@ -494,15 +499,15 @@ theorem riemannCurvature_inner_self_zero -- From hC: 2 g(∇_{[X,Y]} Z, Z) = D_{[X,Y]} f(x) -- ⇒ g(∇_{[X,Y]} Z, Z) = (1/2) D_{[X,Y]} f(x) = (1/2) mDirDeriv f x ([X,Y] x) -- Combine: difference = (1/2) [X(Y(f)) - Y(X(f)) - [X,Y](f)] - inner cross-cancel = 0. - -- Show all four covDeriv HasMetric.metric terms are def-equal to LC.toFun forms: - show metricInner x - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x (X.toFun x)) (Z x) - - metricInner x - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x (Y.toFun x)) (Z x) - - metricInner x - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x + -- Show all four covDeriv g terms are def-equal to LC.toFun forms: + show g.metricInner x + ((leviCivitaConnection (I := I) (M := M) g).toFun + (fun y => covDeriv g Y.toFun Z.toFun y) x (X.toFun x)) (Z x) + - g.metricInner x + ((leviCivitaConnection (I := I) (M := M) g).toFun + (fun y => covDeriv g X.toFun Z.toFun y) x (Y.toFun x)) (Z x) + - g.metricInner x + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x (VectorField.mlieBracket I X.toFun Y.toFun x)) (Z x) = 0 -- Substitute via hA, hB, hC, hHL. @@ -528,49 +533,47 @@ Public-exposure of formerly `private` helper, needed by the Z-slot additivity step of the full 3-slot tensoriality chain (`Riemannian/Curvature/Tensoriality.lean`). -/ theorem riemannCurvature_add_third + (g : RiemannianMetric I M) (X Y Z₁ Z₂ : SmoothVectorField I M) (x : M) : - riemannCurvature HasMetric.metric X.toFun Y.toFun (Z₁ + Z₂).toFun x - = riemannCurvature HasMetric.metric X.toFun Y.toFun Z₁.toFun x - + riemannCurvature HasMetric.metric X.toFun Y.toFun Z₂.toFun x := by + riemannCurvature g X.toFun Y.toFun (Z₁ + Z₂).toFun x + = riemannCurvature g X.toFun Y.toFun Z₁.toFun x + + riemannCurvature g X.toFun Y.toFun Z₂.toFun x := by classical - -- Pi-add of toFun. have h_pi_add : (Z₁ + Z₂).toFun = Z₁.toFun + Z₂.toFun := by funext y; show (Z₁ + Z₂) y = Z₁ y + Z₂ y; rfl - -- Inner section additivity (covDeriv HasMetric.metric Y (Z₁+Z₂) y = covDeriv HasMetric.metric Y Z₁ y + covDeriv HasMetric.metric Y Z₂ y). - have h_inner_Y : (fun y => covDeriv HasMetric.metric Y.toFun (Z₁ + Z₂).toFun y) - = (fun y => covDeriv HasMetric.metric Y.toFun Z₁.toFun y) - + (fun y => covDeriv HasMetric.metric Y.toFun Z₂.toFun y) := by + have h_inner_Y : (fun y => covDeriv g Y.toFun (Z₁ + Z₂).toFun y) + = (fun y => covDeriv g Y.toFun Z₁.toFun y) + + (fun y => covDeriv g Y.toFun Z₂.toFun y) := by funext y rw [h_pi_add] - exact covDeriv_add_field HasMetric.metric Y.toFun Z₁.toFun Z₂.toFun y + exact covDeriv_add_field g Y.toFun Z₁.toFun Z₂.toFun y (Z₁.smoothAt y) (Z₂.smoothAt y) - have h_inner_X : (fun y => covDeriv HasMetric.metric X.toFun (Z₁ + Z₂).toFun y) - = (fun y => covDeriv HasMetric.metric X.toFun Z₁.toFun y) - + (fun y => covDeriv HasMetric.metric X.toFun Z₂.toFun y) := by + have h_inner_X : (fun y => covDeriv g X.toFun (Z₁ + Z₂).toFun y) + = (fun y => covDeriv g X.toFun Z₁.toFun y) + + (fun y => covDeriv g X.toFun Z₂.toFun y) := by funext y rw [h_pi_add] - exact covDeriv_add_field HasMetric.metric X.toFun Z₁.toFun Z₂.toFun y + exact covDeriv_add_field g X.toFun Z₁.toFun Z₂.toFun y (Z₁.smoothAt y) (Z₂.smoothAt y) - -- Unfold riemannCurvature HasMetric.metric. - show covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun (Z₁ + Z₂).toFun y) x - - covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun (Z₁ + Z₂).toFun y) x - - covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) (Z₁ + Z₂).toFun x - = (covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z₁.toFun y) x - - covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z₁.toFun y) x - - covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) Z₁.toFun x) - + (covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z₂.toFun y) x - - covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z₂.toFun y) x - - covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) Z₂.toFun x) + show covDeriv g X.toFun (fun y => covDeriv g Y.toFun (Z₁ + Z₂).toFun y) x + - covDeriv g Y.toFun (fun y => covDeriv g X.toFun (Z₁ + Z₂).toFun y) x + - covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) (Z₁ + Z₂).toFun x + = (covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z₁.toFun y) x + - covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z₁.toFun y) x + - covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z₁.toFun x) + + (covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z₂.toFun y) x + - covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z₂.toFun y) x + - covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z₂.toFun x) rw [h_inner_Y, h_inner_X, h_pi_add] - rw [covDeriv_add_field HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z₁.toFun y) - (fun y => covDeriv HasMetric.metric Y.toFun Z₂.toFun y) x - (covDeriv_smoothVF_smoothAt HasMetric.metric Y Z₁ x) - (covDeriv_smoothVF_smoothAt HasMetric.metric Y Z₂ x), - covDeriv_add_field HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z₁.toFun y) - (fun y => covDeriv HasMetric.metric X.toFun Z₂.toFun y) x - (covDeriv_smoothVF_smoothAt HasMetric.metric X Z₁ x) - (covDeriv_smoothVF_smoothAt HasMetric.metric X Z₂ x), - covDeriv_add_field HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) + rw [covDeriv_add_field g X.toFun (fun y => covDeriv g Y.toFun Z₁.toFun y) + (fun y => covDeriv g Y.toFun Z₂.toFun y) x + (covDeriv_smoothVF_smoothAt g Y Z₁ x) + (covDeriv_smoothVF_smoothAt g Y Z₂ x), + covDeriv_add_field g Y.toFun (fun y => covDeriv g X.toFun Z₁.toFun y) + (fun y => covDeriv g X.toFun Z₂.toFun y) x + (covDeriv_smoothVF_smoothAt g X Z₁ x) + (covDeriv_smoothVF_smoothAt g X Z₂ x), + covDeriv_add_field g (VectorField.mlieBracket I X.toFun Y.toFun) Z₁.toFun Z₂.toFun x (Z₁.smoothAt x) (Z₂.smoothAt x)] abel @@ -590,16 +593,16 @@ theorem riemannCurvature_metric_skew metricInner x (Riem(X.toFun, Y.toFun) Z.toFun x) (W x) + metricInner x (Riem(X.toFun, Y.toFun) W.toFun x) (Z x) = 0 := by -- Diagonal-zero applied to U = Z+W, Z, W. - have h_ZW := riemannCurvature_inner_self_zero X Y (Z + W) x h_interior - have h_Z := riemannCurvature_inner_self_zero X Y Z x h_interior - have h_W := riemannCurvature_inner_self_zero X Y W x h_interior + have h_ZW := riemannCurvature_inner_self_zero HasMetric.metric X Y (Z + W) x h_interior + have h_Z := riemannCurvature_inner_self_zero HasMetric.metric X Y Z x h_interior + have h_W := riemannCurvature_inner_self_zero HasMetric.metric X Y W x h_interior -- Additivity of R in 3rd slot. - have h_add := riemannCurvature_add_third X Y Z W x + have h_add := riemannCurvature_add_third HasMetric.metric X Y Z W x -- (Z+W) x = Z x + W x. have h_ZW_x : (Z + W) x = Z x + W x := rfl -- Expand h_ZW via h_add and h_ZW_x and bilinearity of metricInner. - rw [h_add, h_ZW_x, metricInner_add_left, metricInner_add_right, - metricInner_add_right] at h_ZW + rw [h_add, h_ZW_x, HasMetric.metric.metricInner_add_left, HasMetric.metric.metricInner_add_right, + HasMetric.metric.metricInner_add_right] at h_ZW -- h_ZW : g(R Z, Z) + g(R Z, W) + (g(R W, Z) + g(R W, W)) = 0 linarith @@ -630,7 +633,7 @@ theorem riemannCurvature_pair_symm + metricInner x (Riem(B, C) A x) (D x) + metricInner x (Riem(C, A) B x) (D x) = 0 := by intro A B C D - have h := bianchi_first A B C x + have h := bianchi_first HasMetric.metric A B C x have : metricInner x (Riem(A, B) C x + Riem(B, C) A x + Riem(C, A) B x) (D x) = metricInner x (0 : TangentSpace I x) (D x) := by rw [h] @@ -650,7 +653,7 @@ theorem riemannCurvature_pair_symm metricInner x (Riem(A, B) C x) (D x) = -metricInner x (Riem(B, A) C x) (D x) := by intro A B C D - rw [riemannCurvature_antisymm A B C x, metricInner_neg_left] + rw [riemannCurvature_antisymm HasMetric.metric A B C x, metricInner_neg_left] -- (3,4)-antisymmetry from `riemannCurvature_metric_skew`. have antisym34 : ∀ (A B C D : SmoothVectorField I M), metricInner x (Riem(A, B) C x) (D x) @@ -706,35 +709,30 @@ together with first-pair antisymmetry of $R$ rearranges to the form needed for the Ricci-symmetry trace argument. -/ private lemma riemannCurvature_const_first_swap_eq_neg [IsManifold I 2 M] + (g : RiemannianMetric I M) (v : E) (X Y : SmoothVectorField I M) (x : M) : - riemannCurvature HasMetric.metric (fun _ : M => v) X.toFun Y.toFun x - - riemannCurvature HasMetric.metric (fun _ : M => v) Y.toFun X.toFun x - = -riemannCurvature HasMetric.metric X.toFun Y.toFun (fun _ : M => v) x := by + riemannCurvature g (fun _ : M => v) X.toFun Y.toFun x + - riemannCurvature g (fun _ : M => v) Y.toFun X.toFun x + = -riemannCurvature g X.toFun Y.toFun (fun _ : M => v) x := by classical set V : SmoothVectorField I M := SmoothVectorField.const (I := I) (M := M) v with hV_def - -- Bianchi I with (X', Y', Z') = (V, X, Y). Use the unfolded `V.toFun = fun _ => v` - -- form so the rewrite by `h_antisym` (using the `fun _ => v` shape) fires. - have h_bianchi : riemannCurvature HasMetric.metric (fun _ : M => v) X.toFun Y.toFun x - + riemannCurvature HasMetric.metric X.toFun Y.toFun (fun _ : M => v) x - + riemannCurvature HasMetric.metric Y.toFun (fun _ : M => v) X.toFun x = 0 := - bianchi_first V X Y x - -- First-pair antisymmetry on the 3rd Bianchi summand. + have h_bianchi : riemannCurvature g (fun _ : M => v) X.toFun Y.toFun x + + riemannCurvature g X.toFun Y.toFun (fun _ : M => v) x + + riemannCurvature g Y.toFun (fun _ : M => v) X.toFun x = 0 := + bianchi_first g V X Y x have h_antisym : - riemannCurvature HasMetric.metric Y.toFun (fun _ : M => v) X.toFun x - = -riemannCurvature HasMetric.metric (fun _ : M => v) Y.toFun X.toFun x := - riemannCurvature_antisymm Y.toFun (fun _ : M => v) X.toFun x + riemannCurvature g Y.toFun (fun _ : M => v) X.toFun x + = -riemannCurvature g (fun _ : M => v) Y.toFun X.toFun x := + riemannCurvature_antisymm g Y.toFun (fun _ : M => v) X.toFun x rw [h_antisym] at h_bianchi - -- h_bianchi : R(V,X) Y + R(X,Y) V + - R(V,Y) X = 0 - -- Goal: R(V,X) Y - R(V,Y) X = -R(X,Y) V ⇔ (R(V,X) Y - R(V,Y) X) + R(X,Y) V = 0. apply eq_neg_of_add_eq_zero_left - -- Rearrange h_bianchi via `abel`. - rw [show (riemannCurvature HasMetric.metric (fun _ : M => v) X.toFun Y.toFun x - - riemannCurvature HasMetric.metric (fun _ : M => v) Y.toFun X.toFun x - + riemannCurvature HasMetric.metric X.toFun Y.toFun (fun _ : M => v) x + rw [show (riemannCurvature g (fun _ : M => v) X.toFun Y.toFun x + - riemannCurvature g (fun _ : M => v) Y.toFun X.toFun x + + riemannCurvature g X.toFun Y.toFun (fun _ : M => v) x : TangentSpace I x) - = riemannCurvature HasMetric.metric (fun _ : M => v) X.toFun Y.toFun x - + riemannCurvature HasMetric.metric X.toFun Y.toFun (fun _ : M => v) x - + -riemannCurvature HasMetric.metric (fun _ : M => v) Y.toFun X.toFun x from by abel] + = riemannCurvature g (fun _ : M => v) X.toFun Y.toFun x + + riemannCurvature g X.toFun Y.toFun (fun _ : M => v) x + + -riemannCurvature g (fun _ : M => v) Y.toFun X.toFun x from by abel] exact h_bianchi /-- **Math.** $\mathrm{Ric}(X, Y) = \mathrm{Ric}(Y, X)$. @@ -756,7 +754,7 @@ theorem ricci_symm [IsManifold I 2 M] (X Y : SmoothVectorField I M) (x : M) (h_interior : extChartAt I x x ∈ closure (interior (Set.range I))) : - Ric(X, Y) x = Ric(Y, X) x := by + ricci HasMetric.metric X Y x = ricci HasMetric.metric Y X x := by classical set b := stdOrthonormalBasis ℝ (TangentSpace I x) with hb_def -- Expand each Ricci scalar as `∑ i, ⟪b i, R(const b i, ·) · x⟫_ℝ` via @@ -772,18 +770,16 @@ theorem ricci_symm (curvatureEndo (HasMetric.metric) Y X x) = _ exact LinearMap.trace_eq_sum_inner _ b rw [h_RXY, h_RYX] - -- Per i: the two inner products are equal (their difference vanishes - -- by const-swap Bianchi + diagonal-zero). refine Finset.sum_congr rfl (fun i _ => ?_) rw [← sub_eq_zero, ← inner_sub_right, - riemannCurvature_const_first_swap_eq_neg (I := I) (M := M) (b i : E) X Y x] + riemannCurvature_const_first_swap_eq_neg (I := I) (M := M) HasMetric.metric (b i : E) X Y x] -- Goal: ⟪b i, -R(X, Y) (const b i) x⟫_ℝ = 0 rw [inner_neg_right, neg_eq_zero] -- Goal: ⟪b i, R(X, Y) (const b i) x⟫_ℝ = 0 -- Use real_inner_comm + riemannCurvature_inner_self_zero (with Z = cF[b i]). rw [real_inner_comm] - -- Goal: ⟪R(X, Y) (const b i) x, b i⟫_ℝ = 0 (def-eq metricInner via hm.metric). - exact riemannCurvature_inner_self_zero X Y + -- Goal: ⟪R(X, Y) (const b i) x, b i⟫_ℝ = 0 (def-eq g.metricInner via g). + exact riemannCurvature_inner_self_zero HasMetric.metric X Y (SmoothVectorField.const (I := I) (M := M) (b i : E)) x h_interior @@ -1012,7 +1008,7 @@ theorem IsKilling.second_covDeriv_eq_curvature simpa [A, C] using h have h_curv : C Y Z W - C Z W Y + C W Y Z = 2 * metricInner x (Riem(Y, X) Z x) (W x) := by - have h_bianchi := bianchi_first X W Y x + have h_bianchi := bianchi_first HasMetric.metric X W Y x have h_inner : metricInner x (Riem(X, W) Y x + Riem(W, Y) X x + Riem(Y, X) W x) (Z x) = 0 := by @@ -1028,7 +1024,7 @@ theorem IsKilling.second_covDeriv_eq_curvature have h_antisym12 : metricInner x (Riem(X, Y) Z x) (W x) = -metricInner x (Riem(Y, X) Z x) (W x) := by - rw [riemannCurvature_antisymm X.toFun Y.toFun Z.toFun x, metricInner_neg_left] + rw [riemannCurvature_antisymm HasMetric.metric X.toFun Y.toFun Z.toFun x, metricInner_neg_left] have h_antisym34 : metricInner x (Riem(Y, X) W x) (Z x) = -metricInner x (Riem(Y, X) Z x) (W x) := by diff --git a/OpenGALib/Riemannian/Curvature/Tensoriality.lean b/OpenGALib/Riemannian/Curvature/Tensoriality.lean index b2849f4..3af5e87 100644 --- a/OpenGALib/Riemannian/Curvature/Tensoriality.lean +++ b/OpenGALib/Riemannian/Curvature/Tensoriality.lean @@ -17,7 +17,7 @@ bundled in `riemannCurvature_eq_of_pointwise_eq`. Z-slot Leibniz needs a chart-interior hypothesis (cross-derivative residual closes via manifold scalar Hessian-Lie identity); X-slot -Leibniz does not (covDeriv HasMetric.metric-Leibniz and Lie-bracket-Leibniz cancel +Leibniz does not (covDeriv g-Leibniz and Lie-bracket-Leibniz cancel symmetrically); Y-slot pointwise dependence follows from X-slot via antisymmetry `R(X, Y) = -R(Y, X)`. -/ @@ -37,6 +37,9 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] [T2Space M] [IsLocallyConstantChartedSpace H M] [hm : HasMetric I M] + (g : RiemannianMetric I M) + +include g /-- **Math.** Smoothness of `y ↦ mfderiv f y (V y)` as a scalar function for smooth scalar `f` and smooth tangent section `V`. The directional @@ -44,24 +47,24 @@ derivative `V(f)` is C∞. OpenGALib analog of external `extDerivFun_apply_contMDiff`. Proof routes through the manifold-gradient duality `mfderiv f y v = ⟨∇^M f, v⟩_g`, -which is `metricInner ∘ manifoldGradient ∘ ·`, smooth as a composition. -/ +which is `g.metricInner ∘ manifoldGradient ∘ ·`, smooth as a composition. -/ theorem mfderiv_apply_smoothVF_contMDiff (f : M → ℝ) (V : SmoothVectorField I M) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) : ContMDiff I 𝓘(ℝ, ℝ) ∞ (fun y => (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f y (V.toFun y))) := by - -- Identify with `y ↦ metricInner y (manifoldGradient f y) (V y)` via grad duality. + -- Identify with `y ↦ g.metricInner y (manifoldGradient f y) (V y)` via grad duality. -- Then smoothness follows from manifoldGradient smoothness + V smoothness + -- bilinearity of the metric (encoded in `HasMetric` smoothness). have h_eq : (fun y => (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f y (V.toFun y))) - = (fun y => metricInner y (manifoldGradient (I := I) HasMetric.metric f y) (V.toFun y)) := by + = (fun y => g.metricInner y (manifoldGradient (I := I) g f y) (V.toFun y)) := by funext y - exact (manifoldGradient_inner_eq (I := I) HasMetric.metric f y (V.toFun y)).symm + exact (manifoldGradient_inner_eq (I := I) g f y (V.toFun y)).symm rw [h_eq] - exact fun y => hm.metric.metricInner_contMDiffAt - (n := ∞) (manifoldGradient_smooth_of_smooth (I := I) HasMetric.metric f hf y) (V.smooth y) + exact fun y => g.metricInner_contMDiffAt + (n := ∞) (manifoldGradient_smooth_of_smooth (I := I) g f hf y) (V.smooth y) -/-- **Math.** **3rd-slot (Z-slot) C∞-linearity of `riemannCurvature HasMetric.metric`**: +/-- **Math.** **3rd-slot (Z-slot) C∞-linearity of `riemannCurvature g`**: $$R(X, Y)(f \cdot Z)(x) = f(x) \cdot R(X, Y)\,Z(x).$$ External reference: `riemannSec_smul_third` in @@ -71,8 +74,8 @@ theorem riemannCurvature_smul_third_scalar_field (f : M → ℝ) (X Y Z : SmoothVectorField I M) (x : M) (h_interior : extChartAt I x x ∈ closure (interior (Set.range I))) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) : - riemannCurvature HasMetric.metric X.toFun Y.toFun (f • Z.toFun) x - = f x • riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x := by + riemannCurvature g X.toFun Y.toFun (f • Z.toFun) x + = f x • riemannCurvature g X.toFun Y.toFun Z.toFun x := by classical have hf_at : ∀ y, MDifferentiableAt I 𝓘(ℝ, ℝ) f y := fun y => (hf y).mdifferentiableAt (by simp) @@ -97,35 +100,35 @@ theorem riemannCurvature_smul_third_scalar_field fun y => (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f y (X.toFun y)) with hXf_def -- Smoothness of Yf, Xf as C∞ scalar functions. have hYf_smooth : ContMDiff I 𝓘(ℝ, ℝ) ∞ Yf := - mfderiv_apply_smoothVF_contMDiff (I := I) f Y hf + mfderiv_apply_smoothVF_contMDiff (I := I) g f Y hf have hXf_smooth : ContMDiff I 𝓘(ℝ, ℝ) ∞ Xf := - mfderiv_apply_smoothVF_contMDiff (I := I) f X hf + mfderiv_apply_smoothVF_contMDiff (I := I) g f X hf have hYf_at : MDifferentiableAt I 𝓘(ℝ, ℝ) Yf x := (hYf_smooth x).mdifferentiableAt (by simp) have hXf_at : MDifferentiableAt I 𝓘(ℝ, ℝ) Xf x := (hXf_smooth x).mdifferentiableAt (by simp) -- ∇_V (f Z) section identity at every y (V ∈ {X, Y}). - -- We state as Π-pointwise functions (not lambda-form) to match `covDeriv HasMetric.metric` shape. + -- We state as Π-pointwise functions (not lambda-form) to match `covDeriv g` shape. have h_inner_Y : - covDeriv HasMetric.metric Y.toFun (f • Z.toFun) - = (fun y : M => f y • covDeriv HasMetric.metric Y.toFun Z.toFun y + Yf y • Z.toFun y) := by + covDeriv g Y.toFun (f • Z.toFun) + = (fun y : M => f y • covDeriv g Y.toFun Z.toFun y + Yf y • Z.toFun y) := by funext y - exact covDeriv_smul_scalar_field HasMetric.metric Y.toFun f Z.toFun y (hf_at y) (Z.smoothAt y) + exact covDeriv_smul_scalar_field g Y.toFun f Z.toFun y (hf_at y) (Z.smoothAt y) have h_inner_X : - covDeriv HasMetric.metric X.toFun (f • Z.toFun) - = (fun y : M => f y • covDeriv HasMetric.metric X.toFun Z.toFun y + Xf y • Z.toFun y) := by + covDeriv g X.toFun (f • Z.toFun) + = (fun y : M => f y • covDeriv g X.toFun Z.toFun y + Xf y • Z.toFun y) := by funext y - exact covDeriv_smul_scalar_field HasMetric.metric X.toFun f Z.toFun y (hf_at y) (Z.smoothAt y) + exact covDeriv_smul_scalar_field g X.toFun f Z.toFun y (hf_at y) (Z.smoothAt y) -- Riemann curvature unfold via def. rw [riemannCurvature_commutator_form, riemannCurvature_commutator_form, h_inner_Y, h_inner_X] -- Pointwise sums need to be split into Π-add form for `covDeriv_add_field`. -- The two summands as separate Π-sections. set g1Y : VectorFieldSection I M := - fun y => f y • covDeriv HasMetric.metric Y.toFun Z.toFun y with hg1Y_def + fun y => f y • covDeriv g Y.toFun Z.toFun y with hg1Y_def set g2Y : VectorFieldSection I M := fun y => Yf y • Z.toFun y with hg2Y_def set g1X : VectorFieldSection I M := - fun y => f y • covDeriv HasMetric.metric X.toFun Z.toFun y with hg1X_def + fun y => f y • covDeriv g X.toFun Z.toFun y with hg1X_def set g2X : VectorFieldSection I M := fun y => Xf y • Z.toFun y with hg2X_def -- Convert `fun y => g1Y y + g2Y y` to Π-add `g1Y + g2Y` definitionally. @@ -133,10 +136,10 @@ theorem riemannCurvature_smul_third_scalar_field have h_pi_addX : (fun y : M => g1X y + g2X y) = g1X + g2X := rfl rw [h_pi_addY, h_pi_addX] -- Smoothness witnesses for the summands at x. - have h_dY_Z_smooth : TangentSmoothAt (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x := - covDeriv_smoothVF_smoothAt HasMetric.metric Y Z x - have h_dX_Z_smooth : TangentSmoothAt (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x := - covDeriv_smoothVF_smoothAt HasMetric.metric X Z x + have h_dY_Z_smooth : TangentSmoothAt (fun y => covDeriv g Y.toFun Z.toFun y) x := + covDeriv_smoothVF_smoothAt g Y Z x + have h_dX_Z_smooth : TangentSmoothAt (fun y => covDeriv g X.toFun Z.toFun y) x := + covDeriv_smoothVF_smoothAt g X Z x have hg1Y_smooth : TangentSmoothAt g1Y x := (hf_at x).smul_section h_dY_Z_smooth have hg2Y_smooth : TangentSmoothAt g2Y x := @@ -146,37 +149,37 @@ theorem riemannCurvature_smul_third_scalar_field have hg2X_smooth : TangentSmoothAt g2X x := hXf_at.smul_section (Z.smoothAt x) -- Apply outer additivity (covDeriv_add_field). - rw [covDeriv_add_field HasMetric.metric X.toFun g1Y g2Y x hg1Y_smooth hg2Y_smooth, - covDeriv_add_field HasMetric.metric Y.toFun g1X g2X x hg1X_smooth hg2X_smooth] + rw [covDeriv_add_field g X.toFun g1Y g2Y x hg1Y_smooth hg2Y_smooth, + covDeriv_add_field g Y.toFun g1X g2X x hg1X_smooth hg2X_smooth] -- Apply Leibniz to each summand at x. -- g1Y = f • (∇_Y Z), g2Y = Yf • Z, g1X = f • (∇_X Z), g2X = Xf • Z. -- ∇_X (f • ∇_Y Z) x = f x • ∇_X (∇_Y Z) x + (Xf x) • (∇_Y Z) x. - have hT1_g1Y : covDeriv HasMetric.metric X.toFun g1Y x - = f x • covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x + have hT1_g1Y : covDeriv g X.toFun g1Y x + = f x • covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x + (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f x (X.toFun x)) - • covDeriv HasMetric.metric Y.toFun Z.toFun x := - covDeriv_smul_scalar_field HasMetric.metric X.toFun f - (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x (hf_at x) h_dY_Z_smooth - have hT1_g2Y : covDeriv HasMetric.metric X.toFun g2Y x - = Yf x • covDeriv HasMetric.metric X.toFun Z.toFun x + • covDeriv g Y.toFun Z.toFun x := + covDeriv_smul_scalar_field g X.toFun f + (fun y => covDeriv g Y.toFun Z.toFun y) x (hf_at x) h_dY_Z_smooth + have hT1_g2Y : covDeriv g X.toFun g2Y x + = Yf x • covDeriv g X.toFun Z.toFun x + (show ℝ from mfderiv I 𝓘(ℝ, ℝ) Yf x (X.toFun x)) • Z.toFun x := - covDeriv_smul_scalar_field HasMetric.metric X.toFun Yf Z.toFun x hYf_at (Z.smoothAt x) - have hT2_g1X : covDeriv HasMetric.metric Y.toFun g1X x - = f x • covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x + covDeriv_smul_scalar_field g X.toFun Yf Z.toFun x hYf_at (Z.smoothAt x) + have hT2_g1X : covDeriv g Y.toFun g1X x + = f x • covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x + (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f x (Y.toFun x)) - • covDeriv HasMetric.metric X.toFun Z.toFun x := - covDeriv_smul_scalar_field HasMetric.metric Y.toFun f - (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x (hf_at x) h_dX_Z_smooth - have hT2_g2X : covDeriv HasMetric.metric Y.toFun g2X x - = Xf x • covDeriv HasMetric.metric Y.toFun Z.toFun x + • covDeriv g X.toFun Z.toFun x := + covDeriv_smul_scalar_field g Y.toFun f + (fun y => covDeriv g X.toFun Z.toFun y) x (hf_at x) h_dX_Z_smooth + have hT2_g2X : covDeriv g Y.toFun g2X x + = Xf x • covDeriv g Y.toFun Z.toFun x + (show ℝ from mfderiv I 𝓘(ℝ, ℝ) Xf x (Y.toFun x)) • Z.toFun x := - covDeriv_smul_scalar_field HasMetric.metric Y.toFun Xf Z.toFun x hXf_at (Z.smoothAt x) + covDeriv_smul_scalar_field g Y.toFun Xf Z.toFun x hXf_at (Z.smoothAt x) -- Third term: ∇_{[X,Y]} (f Z) x = f x • ∇_{[X,Y]} Z x + (mfderiv f x ([X,Y] x)) • Z x. - have hT3 : covDeriv HasMetric.metric (mlieBracket I X.toFun Y.toFun) (f • Z.toFun) x - = f x • covDeriv HasMetric.metric (mlieBracket I X.toFun Y.toFun) Z.toFun x + have hT3 : covDeriv g (mlieBracket I X.toFun Y.toFun) (f • Z.toFun) x + = f x • covDeriv g (mlieBracket I X.toFun Y.toFun) Z.toFun x + (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f x (mlieBracket I X.toFun Y.toFun x)) • Z.toFun x := - covDeriv_smul_scalar_field HasMetric.metric (mlieBracket I X.toFun Y.toFun) f Z.toFun x + covDeriv_smul_scalar_field g (mlieBracket I X.toFun Y.toFun) f Z.toFun x (hf_at x) (Z.smoothAt x) rw [hT1_g1Y, hT1_g2Y, hT2_g1X, hT2_g2X, hT3] -- Apply Hessian-Lie identity: X(Yf) x - Y(Xf) x = mfderiv f x ([X,Y] x). @@ -191,44 +194,44 @@ theorem riemannCurvature_smul_third_scalar_field rw [← h_HL, sub_smul] -- Identify `Xf x = mfderiv f x (X x)` and `Yf x = mfderiv f x (Y x)` definitionally -- (both sides reduce by `set ... with` unfolding). - show f x • covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x - + Xf x • covDeriv HasMetric.metric Y.toFun Z.toFun x - + (Yf x • covDeriv HasMetric.metric X.toFun Z.toFun x + show f x • covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x + + Xf x • covDeriv g Y.toFun Z.toFun x + + (Yf x • covDeriv g X.toFun Z.toFun x + (show ℝ from mfderiv I 𝓘(ℝ, ℝ) Yf x (X.toFun x)) • Z.toFun x) - - (f x • covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x - + Yf x • covDeriv HasMetric.metric X.toFun Z.toFun x - + (Xf x • covDeriv HasMetric.metric Y.toFun Z.toFun x + - (f x • covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x + + Yf x • covDeriv g X.toFun Z.toFun x + + (Xf x • covDeriv g Y.toFun Z.toFun x + (show ℝ from mfderiv I 𝓘(ℝ, ℝ) Xf x (Y.toFun x)) • Z.toFun x)) - - (f x • covDeriv HasMetric.metric (mlieBracket I X.toFun Y.toFun) Z.toFun x + - (f x • covDeriv g (mlieBracket I X.toFun Y.toFun) Z.toFun x + ((show ℝ from mfderiv I 𝓘(ℝ, ℝ) Yf x (X.toFun x)) • Z.toFun x - (show ℝ from mfderiv I 𝓘(ℝ, ℝ) Xf x (Y.toFun x)) • Z.toFun x)) - = f x • (covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x - - covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x - - covDeriv HasMetric.metric (mlieBracket I X.toFun Y.toFun) Z.toFun x) + = f x • (covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x + - covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x + - covDeriv g (mlieBracket I X.toFun Y.toFun) Z.toFun x) -- Pure AddCommGroup arithmetic — cross-cancellation + f x • distributes. rw [smul_sub, smul_sub] abel /-! ## Z-slot locality -`riemannCurvature HasMetric.metric` is local in the Z-slot: if `Z =ᶠ[𝓝 x] Z'`, then +`riemannCurvature g` is local in the Z-slot: if `Z =ᶠ[𝓝 x] Z'`, then `R(X, Y) Z(x) = R(X, Y) Z'(x)`. Each of the three terms in `riemannCurvature_commutator_form` satisfies a covariant-derivative locality identity in `Z`: -* `covDeriv HasMetric.metric X (covDeriv HasMetric.metric Y Z) x` and `covDeriv HasMetric.metric Y (covDeriv HasMetric.metric X Z) x` use the - fact that the inner section `covDeriv HasMetric.metric U Z` is locally constant in `Z` +* `covDeriv g X (covDeriv g Y Z) x` and `covDeriv g Y (covDeriv g X Z) x` use the + fact that the inner section `covDeriv g U Z` is locally constant in `Z` (apply `covDeriv_congr_eventuallyEq_field` at every nearby `b`), then - evaluate the outer `covDeriv HasMetric.metric` via the same field-locality lemma. -* `covDeriv HasMetric.metric [X, Y] Z x` reduces directly. -/ + evaluate the outer `covDeriv g` via the same field-locality lemma. +* `covDeriv g [X, Y] Z x` reduces directly. -/ -/-- **Math.** **Z-slot locality of `riemannCurvature HasMetric.metric`**: if `Z =ᶠ[𝓝 x] Z'`, then +/-- **Math.** **Z-slot locality of `riemannCurvature g`**: if `Z =ᶠ[𝓝 x] Z'`, then `R(X, Y) Z(x) = R(X, Y) Z'(x)`. External reference: `riemannSec_eq_of_Z_eventuallyEq` (`differential-geometry/.../CurvatureBundling.lean:227`). -/ theorem riemannCurvature_eq_of_Z_eventuallyEq (X Y Z Z' : SmoothVectorField I M) (x : M) (hZZ' : ∀ᶠ y in 𝓝 x, Z.toFun y = Z'.toFun y) : - riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x - = riemannCurvature HasMetric.metric X.toFun Y.toFun Z'.toFun x := by + riemannCurvature g X.toFun Y.toFun Z.toFun x + = riemannCurvature g X.toFun Y.toFun Z'.toFun x := by classical -- Convert eventual equality to an open nbhd `V'` on which `Z = Z'`. rw [Filter.eventually_iff_exists_mem] at hZZ' @@ -241,50 +244,50 @@ theorem riemannCurvature_eq_of_Z_eventuallyEq (fun b' hb'V' => hZeqZ' b' (hV'U hb'V')) -- Inner section pointwise equality on `V'` (Y- and X-flavored). have h_inner_Y_pt : ∀ b ∈ V', - (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) b - = (fun y => covDeriv HasMetric.metric Y.toFun Z'.toFun y) b := by + (fun y => covDeriv g Y.toFun Z.toFun y) b + = (fun y => covDeriv g Y.toFun Z'.toFun y) b := by intro b hbV' - exact covDeriv_congr_eventuallyEq_field HasMetric.metric Y.toFun Z.toFun Z'.toFun b + exact covDeriv_congr_eventuallyEq_field g Y.toFun Z.toFun Z'.toFun b (Z.smoothAt b) (Z'.smoothAt b) (hZZ'_at b hbV') have h_inner_X_pt : ∀ b ∈ V', - (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) b - = (fun y => covDeriv HasMetric.metric X.toFun Z'.toFun y) b := by + (fun y => covDeriv g X.toFun Z.toFun y) b + = (fun y => covDeriv g X.toFun Z'.toFun y) b := by intro b hbV' - exact covDeriv_congr_eventuallyEq_field HasMetric.metric X.toFun Z.toFun Z'.toFun b + exact covDeriv_congr_eventuallyEq_field g X.toFun Z.toFun Z'.toFun b (Z.smoothAt b) (Z'.smoothAt b) (hZZ'_at b hbV') -- Lift to eventual equality on a nbhd of `x`. have h_inner_Y_ev : ∀ᶠ b in 𝓝 x, - (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) b - = (fun y => covDeriv HasMetric.metric Y.toFun Z'.toFun y) b := + (fun y => covDeriv g Y.toFun Z.toFun y) b + = (fun y => covDeriv g Y.toFun Z'.toFun y) b := Filter.eventually_of_mem (hV'_open.mem_nhds hpV') h_inner_Y_pt have h_inner_X_ev : ∀ᶠ b in 𝓝 x, - (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) b - = (fun y => covDeriv HasMetric.metric X.toFun Z'.toFun y) b := + (fun y => covDeriv g X.toFun Z.toFun y) b + = (fun y => covDeriv g X.toFun Z'.toFun y) b := Filter.eventually_of_mem (hV'_open.mem_nhds hpV') h_inner_X_pt - -- T1: outer `covDeriv HasMetric.metric X ·` field-locality, with `covDeriv_smoothVF_smoothAt` + -- T1: outer `covDeriv g X ·` field-locality, with `covDeriv_smoothVF_smoothAt` -- discharging the inner-section smoothness witnesses. - have hT1 : covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x - = covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z'.toFun y) x := - covDeriv_congr_eventuallyEq_field HasMetric.metric X.toFun - (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) - (fun y => covDeriv HasMetric.metric Y.toFun Z'.toFun y) x - (covDeriv_smoothVF_smoothAt HasMetric.metric Y Z x) - (covDeriv_smoothVF_smoothAt HasMetric.metric Y Z' x) h_inner_Y_ev - -- T2: outer `covDeriv HasMetric.metric Y ·` field-locality. - have hT2 : covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x - = covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z'.toFun y) x := - covDeriv_congr_eventuallyEq_field HasMetric.metric Y.toFun - (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) - (fun y => covDeriv HasMetric.metric X.toFun Z'.toFun y) x - (covDeriv_smoothVF_smoothAt HasMetric.metric X Z x) - (covDeriv_smoothVF_smoothAt HasMetric.metric X Z' x) h_inner_X_ev - -- T3: `covDeriv HasMetric.metric [X, Y] Z x = covDeriv HasMetric.metric [X, Y] Z' x` direct. + have hT1 : covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x + = covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z'.toFun y) x := + covDeriv_congr_eventuallyEq_field g X.toFun + (fun y => covDeriv g Y.toFun Z.toFun y) + (fun y => covDeriv g Y.toFun Z'.toFun y) x + (covDeriv_smoothVF_smoothAt g Y Z x) + (covDeriv_smoothVF_smoothAt g Y Z' x) h_inner_Y_ev + -- T2: outer `covDeriv g Y ·` field-locality. + have hT2 : covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x + = covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z'.toFun y) x := + covDeriv_congr_eventuallyEq_field g Y.toFun + (fun y => covDeriv g X.toFun Z.toFun y) + (fun y => covDeriv g X.toFun Z'.toFun y) x + (covDeriv_smoothVF_smoothAt g X Z x) + (covDeriv_smoothVF_smoothAt g X Z' x) h_inner_X_ev + -- T3: `covDeriv g [X, Y] Z x = covDeriv g [X, Y] Z' x` direct. have hZZ'_x : ∀ᶠ y in 𝓝 x, Z.toFun y = Z'.toFun y := Filter.eventually_of_mem (hV'_open.mem_nhds hpV') (fun b hbV' => hZeqZ' b (hV'U hbV')) - have hT3 : covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x - = covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) Z'.toFun x := - covDeriv_congr_eventuallyEq_field HasMetric.metric + have hT3 : covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x + = covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z'.toFun x := + covDeriv_congr_eventuallyEq_field g (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun Z'.toFun x (Z.smoothAt x) (Z'.smoothAt x) hZZ'_x -- Combine via `riemannCurvature_commutator_form`. @@ -312,7 +315,7 @@ theorem riemannCurvature_eq_zero_of_Z_eq_zero_field (X Y Z : SmoothVectorField I M) (x : M) (h_interior : extChartAt I x x ∈ closure (interior (Set.range I))) (hZx : Z.toFun x = 0) : - riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x = 0 := by + riemannCurvature g X.toFun Y.toFun Z.toFun x = 0 := by classical -- Trivialization at `x`, basis of model fibre, induced local frame. let e := trivializationAt E (TangentSpace I) x @@ -335,10 +338,10 @@ theorem riemannCurvature_eq_zero_of_Z_eq_zero_field let s' : Fin (Module.finrank ℝ E) → SmoothVectorField I M := fun i => { toFun := fun b => χ b • e.localFrame basisF i b smooth := hs'_smooth i } - -- Smoothness of the scalar coefficient `g i b = χ b • coeff i b (Z b)`. - let g : Fin (Module.finrank ℝ E) → M → ℝ := fun i b => + -- Smoothness of the scalar coefficient `c i b = χ b • coeff i b (Z b)`. + let c : Fin (Module.finrank ℝ E) → M → ℝ := fun i b => χ b • e.localFrame_coeff I basisF i b (Z.toFun b) - have hg_smooth : ∀ i, ContMDiff I 𝓘(ℝ, ℝ) ∞ (g i) := by + have hc_smooth : ∀ i, ContMDiff I 𝓘(ℝ, ℝ) ∞ (c i) := by intro i b by_cases hb : b ∈ tsupport (χ : M → ℝ) · have hb_base : b ∈ e.baseSet := hχsupp hb @@ -348,7 +351,7 @@ theorem riemannCurvature_eq_zero_of_Z_eq_zero_field ((LinearMap.piApply (e.localFrame_coeff I basisF i)) Z.toFun) b := contMDiffAt_localFrame_coeff basisF hb_base (Z.smooth b) i exact hχ_at.smul hcoeff_at - · -- Outside `tsupport χ`, `χ = 0` near `b`, so `g i = 0` near `b`. + · -- Outside `tsupport χ`, `χ = 0` near `b`, so `c i = 0` near `b`. have hχ_zero : ∀ᶠ y in nhds b, (χ : M → ℝ) y = 0 := by apply Filter.Eventually.mono ((isClosed_tsupport (χ : M → ℝ)).isOpen_compl.mem_nhds hb) @@ -358,15 +361,15 @@ theorem riemannCurvature_eq_zero_of_Z_eq_zero_field filter_upwards [hχ_zero] with y hy show χ y • e.localFrame_coeff I basisF i y (Z.toFun y) = 0 rw [hy, zero_smul] - -- `g i x = 0` from `Z x = 0` and linearity of `localFrame_coeff`. - have hg_zero : ∀ i, g i x = 0 := by + -- `c i x = 0` from `Z x = 0` and linearity of `localFrame_coeff`. + have hc_zero : ∀ i, c i x = 0 := by intro i show χ x • e.localFrame_coeff I basisF i x (Z.toFun x) = 0 rw [hZx, map_zero, smul_zero] -- `Z =ᶠ ∑ g_i • s'_i` near `x`: on a nbhd where `χ = 1` and `b ∈ e.baseSet`, -- the sum reduces to `eq_sum_localFrame_coeff_smul`. have hZ_eq_sum : ∀ᶠ b in 𝓝 x, - Z.toFun b = ∑ i, g i b • (s' i).toFun b := by + Z.toFun b = ∑ i, c i b • (s' i).toFun b := by filter_upwards [χ.eventuallyEq_one, e.open_baseSet.mem_nhds he_mem] with b hχb hb_base show Z.toFun b @@ -377,110 +380,110 @@ theorem riemannCurvature_eq_zero_of_Z_eq_zero_field exact e.eq_sum_localFrame_coeff_smul (b := basisF) hb_base -- Wrap the finite sum as a `SmoothVectorField`. have hZsum_smooth : ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ - (fun b : M => (⟨b, ∑ i, g i b • (s' i).toFun b⟩ : TangentBundle I M)) := by + (fun b : M => (⟨b, ∑ i, c i b • (s' i).toFun b⟩ : TangentBundle I M)) := by refine ContMDiff.sum_section (s := Finset.univ) ?_ intro i _ - exact (hg_smooth i).smul_section (hs'_smooth i) + exact (hc_smooth i).smul_section (hs'_smooth i) let Zsum : SmoothVectorField I M := - { toFun := fun b => ∑ i, g i b • (s' i).toFun b + { toFun := fun b => ∑ i, c i b • (s' i).toFun b smooth := hZsum_smooth } -- Z-slot locality reduces to the sum form. - rw [riemannCurvature_eq_of_Z_eventuallyEq X Y Z Zsum x hZ_eq_sum] + rw [riemannCurvature_eq_of_Z_eventuallyEq g X Y Z Zsum x hZ_eq_sum] -- Induct on the Finset, splitting summands and applying Z-slot Leibniz + additivity. - show riemannCurvature HasMetric.metric X.toFun Y.toFun + show riemannCurvature g X.toFun Y.toFun (fun b => ∑ i ∈ (Finset.univ : Finset (Fin (Module.finrank ℝ E))), - g i b • (s' i).toFun b) x = 0 + c i b • (s' i).toFun b) x = 0 -- The generalized induction statement. suffices h : ∀ (T : Finset (Fin (Module.finrank ℝ E))), - riemannCurvature HasMetric.metric X.toFun Y.toFun - (fun b => ∑ i ∈ T, g i b • (s' i).toFun b) x - = ∑ i ∈ T, g i x • riemannCurvature HasMetric.metric X.toFun Y.toFun (s' i).toFun x by + riemannCurvature g X.toFun Y.toFun + (fun b => ∑ i ∈ T, c i b • (s' i).toFun b) x + = ∑ i ∈ T, c i x • riemannCurvature g X.toFun Y.toFun (s' i).toFun x by rw [h Finset.univ] apply Finset.sum_eq_zero intro i _ - rw [hg_zero i, zero_smul] + rw [hc_zero i, zero_smul] intro T induction T using Finset.induction_on with | empty => -- Goal: R(X, Y) (fun _ => 0) x = 0. simp only [Finset.sum_empty] -- Identify `fun _ : M => (0 : TangentSpace I _)` with the zero global section. - show riemannCurvature HasMetric.metric X.toFun Y.toFun (fun _ : M => (0 : TangentSpace I _)) x = 0 - -- Each `covDeriv HasMetric.metric U (fun _ => 0)` is the zero section pointwise. + show riemannCurvature g X.toFun Y.toFun (fun _ : M => (0 : TangentSpace I _)) x = 0 + -- Each `covDeriv g U (fun _ => 0)` is the zero section pointwise. have h_zero_outer : ∀ U V : VectorFieldSection I M, - covDeriv HasMetric.metric U (fun y : M => - covDeriv HasMetric.metric V (fun _ : M => (0 : TangentSpace I _)) y) x = 0 := by + covDeriv g U (fun y : M => + covDeriv g V (fun _ : M => (0 : TangentSpace I _)) y) x = 0 := by intro U V -- Inner section is the zero section. have h_inner : (fun y : M => - covDeriv HasMetric.metric V (fun _ : M => (0 : TangentSpace I _)) y) + covDeriv g V (fun _ : M => (0 : TangentSpace I _)) y) = (fun _ : M => (0 : TangentSpace I _)) := by funext y - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun _ : M => (0 : TangentSpace I _)) y) (V y) = 0 - have h0 : (leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun _ : M => (0 : TangentSpace I _)) y = 0 := - (leviCivitaConnection (I := I) (M := M) HasMetric.metric).isCovariantDerivativeOnUniv.zero (x := y) + show ((leviCivitaConnection (I := I) (M := M) g).toFun (fun _ : M => (0 : TangentSpace I _)) y) (V y) = 0 + have h0 : (leviCivitaConnection (I := I) (M := M) g).toFun (fun _ : M => (0 : TangentSpace I _)) y = 0 := + (leviCivitaConnection (I := I) (M := M) g).isCovariantDerivativeOnUniv.zero (x := y) rw [h0]; rfl rw [h_inner] - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun _ : M => (0 : TangentSpace I _)) x) (U x) = 0 - have h0 : (leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun _ : M => (0 : TangentSpace I _)) x = 0 := - (leviCivitaConnection (I := I) (M := M) HasMetric.metric).isCovariantDerivativeOnUniv.zero (x := x) + show ((leviCivitaConnection (I := I) (M := M) g).toFun (fun _ : M => (0 : TangentSpace I _)) x) (U x) = 0 + have h0 : (leviCivitaConnection (I := I) (M := M) g).toFun (fun _ : M => (0 : TangentSpace I _)) x = 0 := + (leviCivitaConnection (I := I) (M := M) g).isCovariantDerivativeOnUniv.zero (x := x) rw [h0]; rfl have h_zero_third : - covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) + covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) (fun _ : M => (0 : TangentSpace I _)) x = 0 := by - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun _ : M => (0 : TangentSpace I _)) x) + show ((leviCivitaConnection (I := I) (M := M) g).toFun (fun _ : M => (0 : TangentSpace I _)) x) (VectorField.mlieBracket I X.toFun Y.toFun x) = 0 - have h0 : (leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun _ : M => (0 : TangentSpace I _)) x = 0 := - (leviCivitaConnection (I := I) (M := M) HasMetric.metric).isCovariantDerivativeOnUniv.zero (x := x) + have h0 : (leviCivitaConnection (I := I) (M := M) g).toFun (fun _ : M => (0 : TangentSpace I _)) x = 0 := + (leviCivitaConnection (I := I) (M := M) g).isCovariantDerivativeOnUniv.zero (x := x) rw [h0]; rfl rw [riemannCurvature_commutator_form, h_zero_outer X.toFun Y.toFun, h_zero_outer Y.toFun X.toFun, h_zero_third] abel | insert j s hjs IH => - -- Split `∑_{insert j s} = g j • s'_j + ∑_s` via `Finset.sum_insert`. - have hsplit : (fun b : M => ∑ i ∈ insert j s, g i b • (s' i).toFun b) - = ((g j • (s' j).toFun : Π b, TangentSpace I b) - + (fun b : M => ∑ i ∈ s, g i b • (s' i).toFun b)) := by + -- Split `∑_{insert j s} = c j • s'_j + ∑_s` via `Finset.sum_insert`. + have hsplit : (fun b : M => ∑ i ∈ insert j s, c i b • (s' i).toFun b) + = ((c j • (s' j).toFun : Π b, TangentSpace I b) + + (fun b : M => ∑ i ∈ s, c i b • (s' i).toFun b)) := by funext b - change ∑ i ∈ insert j s, g i b • (s' i).toFun b - = g j b • (s' j).toFun b + ∑ i ∈ s, g i b • (s' i).toFun b + change ∑ i ∈ insert j s, c i b • (s' i).toFun b + = c j b • (s' j).toFun b + ∑ i ∈ s, c i b • (s' i).toFun b rw [Finset.sum_insert hjs] rw [hsplit] -- Wrap the head summand and the tail as `SmoothVectorField`. have hgj_smooth_section : ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ - (fun b : M => (⟨b, g j b • (s' j).toFun b⟩ : TangentBundle I M)) := - (hg_smooth j).smul_section (hs'_smooth j) + (fun b : M => (⟨b, c j b • (s' j).toFun b⟩ : TangentBundle I M)) := + (hc_smooth j).smul_section (hs'_smooth j) have hrest_smooth : ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ - (fun b : M => (⟨b, ∑ i ∈ s, g i b • (s' i).toFun b⟩ : TangentBundle I M)) := by + (fun b : M => (⟨b, ∑ i ∈ s, c i b • (s' i).toFun b⟩ : TangentBundle I M)) := by refine ContMDiff.sum_section (s := s) ?_ intro i _ - exact (hg_smooth i).smul_section (hs'_smooth i) + exact (hc_smooth i).smul_section (hs'_smooth i) let gjs : SmoothVectorField I M := - { toFun := fun b => g j b • (s' j).toFun b, smooth := hgj_smooth_section } + { toFun := fun b => c j b • (s' j).toFun b, smooth := hgj_smooth_section } let rest : SmoothVectorField I M := - { toFun := fun b => ∑ i ∈ s, g i b • (s' i).toFun b, smooth := hrest_smooth } - show riemannCurvature HasMetric.metric X.toFun Y.toFun (gjs.toFun + rest.toFun) x - = ∑ i ∈ insert j s, g i x • riemannCurvature HasMetric.metric X.toFun Y.toFun (s' i).toFun x + { toFun := fun b => ∑ i ∈ s, c i b • (s' i).toFun b, smooth := hrest_smooth } + show riemannCurvature g X.toFun Y.toFun (gjs.toFun + rest.toFun) x + = ∑ i ∈ insert j s, c i x • riemannCurvature g X.toFun Y.toFun (s' i).toFun x -- Z-slot additivity on the sum head + tail. have h_add : - riemannCurvature HasMetric.metric X.toFun Y.toFun (gjs.toFun + rest.toFun) x - = riemannCurvature HasMetric.metric X.toFun Y.toFun gjs.toFun x - + riemannCurvature HasMetric.metric X.toFun Y.toFun rest.toFun x := by - have := riemannCurvature_add_third X Y gjs rest x + riemannCurvature g X.toFun Y.toFun (gjs.toFun + rest.toFun) x + = riemannCurvature g X.toFun Y.toFun gjs.toFun x + + riemannCurvature g X.toFun Y.toFun rest.toFun x := by + have := riemannCurvature_add_third g X Y gjs rest x simpa using this - -- Z-slot scalar Leibniz on the head: R(X, Y) (g j • s' j) x = g j x • R(X, Y) (s' j) x. + -- Z-slot scalar Leibniz on the head: R(X, Y) (c j • s' j) x = c j x • R(X, Y) (s' j) x. have h_smul : - riemannCurvature HasMetric.metric X.toFun Y.toFun gjs.toFun x - = g j x • riemannCurvature HasMetric.metric X.toFun Y.toFun (s' j).toFun x := by - show riemannCurvature HasMetric.metric X.toFun Y.toFun (g j • (s' j).toFun) x - = g j x • riemannCurvature HasMetric.metric X.toFun Y.toFun (s' j).toFun x + riemannCurvature g X.toFun Y.toFun gjs.toFun x + = c j x • riemannCurvature g X.toFun Y.toFun (s' j).toFun x := by + show riemannCurvature g X.toFun Y.toFun (c j • (s' j).toFun) x + = c j x • riemannCurvature g X.toFun Y.toFun (s' j).toFun x exact riemannCurvature_smul_third_scalar_field - (g j) X Y (s' j) x h_interior (hg_smooth j) + g (c j) X Y (s' j) x h_interior (hc_smooth j) rw [h_add, h_smul, IH, Finset.sum_insert hjs] /-! ## Z-slot pointwise dependence -`riemannCurvature HasMetric.metric` at `x` depends only on `Z(x)` (modulo smoothness of `Z`): +`riemannCurvature g` at `x` depends only on `Z(x)` (modulo smoothness of `Z`): if `Z x = Z' x`, then `R(X, Y) Z(x) = R(X, Y) Z'(x)`. Derived from Z-slot vanishing on `τ := Z - Z'` combined with Z-slot additivity. -/ @@ -490,15 +493,15 @@ theorem riemannCurvature_eq_of_Z_eq_at (X Y Z Z' : SmoothVectorField I M) (x : M) (h_interior : extChartAt I x x ∈ closure (interior (Set.range I))) (hZZ' : Z.toFun x = Z'.toFun x) : - riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x - = riemannCurvature HasMetric.metric X.toFun Y.toFun Z'.toFun x := by + riemannCurvature g X.toFun Y.toFun Z.toFun x + = riemannCurvature g X.toFun Y.toFun Z'.toFun x := by -- `τ := Z - Z'` is smooth with `τ x = 0`. let τ : SmoothVectorField I M := Z - Z' have hτ_zero : τ.toFun x = 0 := by show Z.toFun x - Z'.toFun x = 0 rw [hZZ']; abel - have hτ_vanish : riemannCurvature HasMetric.metric X.toFun Y.toFun τ.toFun x = 0 := - riemannCurvature_eq_zero_of_Z_eq_zero_field X Y τ x h_interior hτ_zero + have hτ_vanish : riemannCurvature g X.toFun Y.toFun τ.toFun x = 0 := + riemannCurvature_eq_zero_of_Z_eq_zero_field g X Y τ x h_interior hτ_zero -- `Z = Z' + τ` pointwise; transfer to `(Z' + τ).toFun = Z.toFun` via the -- SmoothVectorField `Add` instance (defn-equality `(Z' + τ).toFun y = Z'.toFun y + τ.toFun y`). have h_pi : (Z' + τ).toFun = Z.toFun := by @@ -506,22 +509,22 @@ theorem riemannCurvature_eq_of_Z_eq_at show Z'.toFun y + (Z.toFun y - Z'.toFun y) = Z.toFun y abel -- Apply Z-slot additivity on `Z' + τ` and rewrite `(Z' + τ).toFun` to `Z.toFun`. - have h_add := riemannCurvature_add_third X Y Z' τ x + have h_add := riemannCurvature_add_third g X Y Z' τ x rw [h_pi] at h_add rw [h_add, hτ_vanish, add_zero] /-! ## First-slot tensoriality -The X-slot of `riemannCurvature HasMetric.metric` admits clean scalar Leibniz: the boundary +The X-slot of `riemannCurvature g` admits clean scalar Leibniz: the boundary terms cancel symmetrically between the inner-section Leibniz and the Lie-bracket Leibniz, leaving no curvature correction. External reference: `riemannSec_smul_left` and `riemannSec_add_left` in `differential-geometry/.../Curvature.lean`. -/ -/-- **Math.** **First-slot scalar Leibniz** for `riemannCurvature HasMetric.metric`: +/-- **Math.** **First-slot scalar Leibniz** for `riemannCurvature g`: $$R(f \cdot X, Y) Z(x) = f(x) \cdot R(X, Y) Z(x).$$ -Clean cancellation: the cross-derivative residual from the inner `covDeriv HasMetric.metric` +Clean cancellation: the cross-derivative residual from the inner `covDeriv g` Leibniz pairs against the Lie-bracket smul-Leibniz with opposite sign. In contrast to `riemannCurvature_smul_third_scalar_field`, the X-slot @@ -530,38 +533,38 @@ theorem riemannCurvature_smul_first_scalar_field [IsManifold I 2 M] (f : M → ℝ) (X Y Z : SmoothVectorField I M) (x : M) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) : - riemannCurvature HasMetric.metric (f • X.toFun) Y.toFun Z.toFun x - = f x • riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x := by + riemannCurvature g (f • X.toFun) Y.toFun Z.toFun x + = f x • riemannCurvature g X.toFun Y.toFun Z.toFun x := by classical have hf_at : MDifferentiableAt I 𝓘(ℝ, ℝ) f x := (hf x).mdifferentiableAt (by simp) -- Directional derivative `Yf(x)`. set Yf_x : ℝ := (show ℝ from mfderiv I 𝓘(ℝ, ℝ) f x (Y.toFun x)) with hYf_def - -- T1: covDeriv HasMetric.metric (f • X) (∇_Y Z) x = f x • covDeriv HasMetric.metric X (∇_Y Z) x via direction continuous linear map. - have hT1 : covDeriv HasMetric.metric (f • X.toFun) (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x - = f x • covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x := by - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x) + -- T1: covDeriv g (f • X) (∇_Y Z) x = f x • covDeriv g X (∇_Y Z) x via direction continuous linear map. + have hT1 : covDeriv g (f • X.toFun) (fun y => covDeriv g Y.toFun Z.toFun y) x + = f x • covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x := by + show ((leviCivitaConnection (I := I) (M := M) g).toFun (fun y => covDeriv g Y.toFun Z.toFun y) x) ((f • X.toFun) x) - = f x • ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x) + = f x • ((leviCivitaConnection (I := I) (M := M) g).toFun (fun y => covDeriv g Y.toFun Z.toFun y) x) (X.toFun x) rw [show (f • X.toFun) x = f x • X.toFun x from rfl, map_smul] - -- T2: inner section `covDeriv HasMetric.metric (f • X) Z = f • (covDeriv HasMetric.metric X Z)` pointwise. + -- T2: inner section `covDeriv g (f • X) Z = f • (covDeriv g X Z)` pointwise. have h_inner : - (fun y => covDeriv HasMetric.metric (f • X.toFun) Z.toFun y) - = f • (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) := by + (fun y => covDeriv g (f • X.toFun) Z.toFun y) + = f • (fun y => covDeriv g X.toFun Z.toFun y) := by funext y - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y) ((f • X.toFun) y) - = f y • ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y) (X.toFun y) + show ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y) ((f • X.toFun) y) + = f y • ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y) (X.toFun y) rw [show (f • X.toFun) y = f y • X.toFun y from rfl, map_smul] - -- T2: covDeriv HasMetric.metric Y (f • cov X Z) x = f x • cov Y (cov X Z) x + Yf_x • cov X Z x. + -- T2: covDeriv g Y (f • cov X Z) x = f x • cov Y (cov X Z) x + Yf_x • cov X Z x. have hT2 : - covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric (f • X.toFun) Z.toFun y) x - = f x • covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x - + Yf_x • covDeriv HasMetric.metric X.toFun Z.toFun x := by + covDeriv g Y.toFun (fun y => covDeriv g (f • X.toFun) Z.toFun y) x + = f x • covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x + + Yf_x • covDeriv g X.toFun Z.toFun x := by rw [h_inner] - exact covDeriv_smul_scalar_field HasMetric.metric Y.toFun f - (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x hf_at - (covDeriv_smoothVF_smoothAt HasMetric.metric X Z x) + exact covDeriv_smul_scalar_field g Y.toFun f + (fun y => covDeriv g X.toFun Z.toFun y) x hf_at + (covDeriv_smoothVF_smoothAt g X Z x) -- Lie-bracket smul: `[f • X, Y] x = -Yf_x • X x + f x • [X, Y] x`. have h_br : VectorField.mlieBracket I (f • X.toFun) Y.toFun x = -Yf_x • X.toFun x + f x • VectorField.mlieBracket I X.toFun Y.toFun x := by @@ -572,15 +575,15 @@ theorem riemannCurvature_smul_first_scalar_field = -(show ℝ from mfderiv I 𝓘(ℝ, ℝ) f x (Y.toFun x)) • X.toFun x + f x • VectorField.mlieBracket I X.toFun Y.toFun x convert h using 2 - -- T3: covDeriv HasMetric.metric [f • X, Y] Z x = -Yf_x • cov X Z x + f x • cov [X, Y] Z x via continuous linear map. + -- T3: covDeriv g [f • X, Y] Z x = -Yf_x • cov X Z x + f x • cov [X, Y] Z x via continuous linear map. have hT3 : - covDeriv HasMetric.metric (VectorField.mlieBracket I (f • X.toFun) Y.toFun) Z.toFun x - = -Yf_x • covDeriv HasMetric.metric X.toFun Z.toFun x - + f x • covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x := by - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x) + covDeriv g (VectorField.mlieBracket I (f • X.toFun) Y.toFun) Z.toFun x + = -Yf_x • covDeriv g X.toFun Z.toFun x + + f x • covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x := by + show ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x) (VectorField.mlieBracket I (f • X.toFun) Y.toFun x) - = -Yf_x • ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x) (X.toFun x) - + f x • ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x) + = -Yf_x • ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x) (X.toFun x) + + f x • ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x) (VectorField.mlieBracket I X.toFun Y.toFun x) rw [h_br, map_add, map_smul, map_smul] -- Assemble: 3 terms cancel the `Yf_x` boundary contribution symmetrically. @@ -591,44 +594,44 @@ theorem riemannCurvature_smul_first_scalar_field simp only [neg_smul] abel -/-- **Math.** **First-slot additivity** for `riemannCurvature HasMetric.metric`: $R(X + X', Y) Z = R(X, Y) Z + R(X', Y) Z$. -/ +/-- **Math.** **First-slot additivity** for `riemannCurvature g`: $R(X + X', Y) Z = R(X, Y) Z + R(X', Y) Z$. -/ theorem riemannCurvature_add_first (X X' Y Z : SmoothVectorField I M) (x : M) : - riemannCurvature HasMetric.metric (X + X').toFun Y.toFun Z.toFun x - = riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x - + riemannCurvature HasMetric.metric X'.toFun Y.toFun Z.toFun x := by + riemannCurvature g (X + X').toFun Y.toFun Z.toFun x + = riemannCurvature g X.toFun Y.toFun Z.toFun x + + riemannCurvature g X'.toFun Y.toFun Z.toFun x := by classical -- Pi-add unfolds. have h_pi_add : (X + X').toFun = X.toFun + X'.toFun := by funext y; rfl -- T1: cov (X + X') (∇_Y Z) x = cov X (∇_Y Z) x + cov X' (∇_Y Z) x via direction continuous linear map add. - have hT1 : covDeriv HasMetric.metric (X + X').toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x - = covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x - + covDeriv HasMetric.metric X'.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x := by - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x) + have hT1 : covDeriv g (X + X').toFun (fun y => covDeriv g Y.toFun Z.toFun y) x + = covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x + + covDeriv g X'.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x := by + show ((leviCivitaConnection (I := I) (M := M) g).toFun (fun y => covDeriv g Y.toFun Z.toFun y) x) ((X + X').toFun x) - = ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x) (X.toFun x) - + ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x) (X'.toFun x) + = ((leviCivitaConnection (I := I) (M := M) g).toFun (fun y => covDeriv g Y.toFun Z.toFun y) x) (X.toFun x) + + ((leviCivitaConnection (I := I) (M := M) g).toFun (fun y => covDeriv g Y.toFun Z.toFun y) x) (X'.toFun x) rw [show (X + X').toFun x = X.toFun x + X'.toFun x from rfl, map_add] -- Inner section: cov (X + X') Z = cov X Z + cov X' Z via direction continuous linear map add. have h_inner : - (fun y => covDeriv HasMetric.metric (X + X').toFun Z.toFun y) - = (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) + (fun y => covDeriv HasMetric.metric X'.toFun Z.toFun y) := by + (fun y => covDeriv g (X + X').toFun Z.toFun y) + = (fun y => covDeriv g X.toFun Z.toFun y) + (fun y => covDeriv g X'.toFun Z.toFun y) := by funext y - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y) ((X + X').toFun y) - = ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y) (X.toFun y) - + ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y) (X'.toFun y) + show ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y) ((X + X').toFun y) + = ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y) (X.toFun y) + + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y) (X'.toFun y) rw [show (X + X').toFun y = X.toFun y + X'.toFun y from rfl, map_add] -- T2: outer cov_add. have hT2 : - covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric (X + X').toFun Z.toFun y) x - = covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x - + covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X'.toFun Z.toFun y) x := by + covDeriv g Y.toFun (fun y => covDeriv g (X + X').toFun Z.toFun y) x + = covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x + + covDeriv g Y.toFun (fun y => covDeriv g X'.toFun Z.toFun y) x := by rw [h_inner] - exact covDeriv_add_field HasMetric.metric Y.toFun - (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) - (fun y => covDeriv HasMetric.metric X'.toFun Z.toFun y) x - (covDeriv_smoothVF_smoothAt HasMetric.metric X Z x) - (covDeriv_smoothVF_smoothAt HasMetric.metric X' Z x) + exact covDeriv_add_field g Y.toFun + (fun y => covDeriv g X.toFun Z.toFun y) + (fun y => covDeriv g X'.toFun Z.toFun y) x + (covDeriv_smoothVF_smoothAt g X Z x) + (covDeriv_smoothVF_smoothAt g X' Z x) -- Lie-bracket additivity: [X + X', Y] x = [X, Y] x + [X', Y] x. have h_br : VectorField.mlieBracket I (X + X').toFun Y.toFun x = VectorField.mlieBracket I X.toFun Y.toFun x @@ -638,20 +641,20 @@ theorem riemannCurvature_add_first (W := Y.toFun) (x := x) (X.smoothAt x) (X'.smoothAt x) -- T3: cov [X+X', Y] Z x = cov [X, Y] Z x + cov [X', Y] Z x via continuous linear map add. have hT3 : - covDeriv HasMetric.metric (VectorField.mlieBracket I (X + X').toFun Y.toFun) Z.toFun x - = covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x - + covDeriv HasMetric.metric (VectorField.mlieBracket I X'.toFun Y.toFun) Z.toFun x := by - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x) + covDeriv g (VectorField.mlieBracket I (X + X').toFun Y.toFun) Z.toFun x + = covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x + + covDeriv g (VectorField.mlieBracket I X'.toFun Y.toFun) Z.toFun x := by + show ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x) (VectorField.mlieBracket I (X + X').toFun Y.toFun x) - = ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x) + = ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x) (VectorField.mlieBracket I X.toFun Y.toFun x) - + ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x) + + ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x) (VectorField.mlieBracket I X'.toFun Y.toFun x) rw [h_br, map_add] rw [riemannCurvature_commutator_form, hT1, hT2, hT3, riemannCurvature_commutator_form, riemannCurvature_commutator_form] abel -/-- **Math.** **X-slot locality of `riemannCurvature HasMetric.metric`**: if `X =ᶠ[𝓝 x] X'`, then +/-- **Math.** **X-slot locality of `riemannCurvature g`**: if `X =ᶠ[𝓝 x] X'`, then `R(X, Y) Z(x) = R(X', Y) Z(x)`. Compared to Z-slot locality, the X-slot proof is short — terms T1 and T3 depend on `X` only pointwise at `x` (since the direction enters as `(lc.toFun ... x)(X x)`), and T2 reduces @@ -659,43 +662,43 @@ via inner-section locality plus `covDeriv_congr_eventuallyEq_field`. -/ theorem riemannCurvature_eq_of_X_eventuallyEq (X X' Y Z : SmoothVectorField I M) (x : M) (hXX' : ∀ᶠ y in 𝓝 x, X.toFun y = X'.toFun y) : - riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x - = riemannCurvature HasMetric.metric X'.toFun Y.toFun Z.toFun x := by + riemannCurvature g X.toFun Y.toFun Z.toFun x + = riemannCurvature g X'.toFun Y.toFun Z.toFun x := by classical have hXx : X.toFun x = X'.toFun x := hXX'.self_of_nhds -- T1: direction continuous linear map application — only `X x` matters. - have hT1 : covDeriv HasMetric.metric X.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x - = covDeriv HasMetric.metric X'.toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x := by - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x) + have hT1 : covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x + = covDeriv g X'.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x := by + show ((leviCivitaConnection (I := I) (M := M) g).toFun (fun y => covDeriv g Y.toFun Z.toFun y) x) (X.toFun x) - = ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x) + = ((leviCivitaConnection (I := I) (M := M) g).toFun (fun y => covDeriv g Y.toFun Z.toFun y) x) (X'.toFun x) rw [hXx] - -- T2: inner section locality + outer covDeriv HasMetric.metric field-locality. - -- `covDeriv HasMetric.metric X Z =ᶠ covDeriv HasMetric.metric X' Z` near x via X-pointwise direction continuous linear map. + -- T2: inner section locality + outer covDeriv g field-locality. + -- `covDeriv g X Z =ᶠ covDeriv g X' Z` near x via X-pointwise direction continuous linear map. have h_inner_ev : ∀ᶠ y in 𝓝 x, - (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) y = (fun y => covDeriv HasMetric.metric X'.toFun Z.toFun y) y := by + (fun y => covDeriv g X.toFun Z.toFun y) y = (fun y => covDeriv g X'.toFun Z.toFun y) y := by filter_upwards [hXX'] with y hy - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y) (X.toFun y) - = ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y) (X'.toFun y) + show ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y) (X.toFun y) + = ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y) (X'.toFun y) rw [hy] - have hT2 : covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) x - = covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric X'.toFun Z.toFun y) x := - covDeriv_congr_eventuallyEq_field HasMetric.metric Y.toFun - (fun y => covDeriv HasMetric.metric X.toFun Z.toFun y) - (fun y => covDeriv HasMetric.metric X'.toFun Z.toFun y) x - (covDeriv_smoothVF_smoothAt HasMetric.metric X Z x) - (covDeriv_smoothVF_smoothAt HasMetric.metric X' Z x) h_inner_ev + have hT2 : covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x + = covDeriv g Y.toFun (fun y => covDeriv g X'.toFun Z.toFun y) x := + covDeriv_congr_eventuallyEq_field g Y.toFun + (fun y => covDeriv g X.toFun Z.toFun y) + (fun y => covDeriv g X'.toFun Z.toFun y) x + (covDeriv_smoothVF_smoothAt g X Z x) + (covDeriv_smoothVF_smoothAt g X' Z x) h_inner_ev -- T3: `[X, Y] x = [X', Y] x` from pointwise X equality + Lie-bracket eventuallyEq. have h_br_x : VectorField.mlieBracket I X.toFun Y.toFun x = VectorField.mlieBracket I X'.toFun Y.toFun x := Filter.EventuallyEq.mlieBracket_vectorField_eq (I := I) hXX' (Filter.EventuallyEq.refl _ Y.toFun) - have hT3 : covDeriv HasMetric.metric (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x - = covDeriv HasMetric.metric (VectorField.mlieBracket I X'.toFun Y.toFun) Z.toFun x := by - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x) + have hT3 : covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x + = covDeriv g (VectorField.mlieBracket I X'.toFun Y.toFun) Z.toFun x := by + show ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x) (VectorField.mlieBracket I X.toFun Y.toFun x) - = ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x) + = ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x) (VectorField.mlieBracket I X'.toFun Y.toFun x) rw [h_br_x] rw [riemannCurvature_commutator_form, riemannCurvature_commutator_form, hT1, hT2, hT3] @@ -717,7 +720,7 @@ theorem riemannCurvature_eq_zero_of_X_eq_zero_field [IsManifold I 2 M] [T2Space M] (X Y Z : SmoothVectorField I M) (x : M) (hXx : X.toFun x = 0) : - riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x = 0 := by + riemannCurvature g X.toFun Y.toFun Z.toFun x = 0 := by classical let e := trivializationAt E (TangentSpace I) x have he_mem : x ∈ e.baseSet := mem_baseSet_trivializationAt E _ x @@ -737,10 +740,10 @@ theorem riemannCurvature_eq_zero_of_X_eq_zero_field let s' : Fin (Module.finrank ℝ E) → SmoothVectorField I M := fun i => { toFun := fun b => χ b • e.localFrame basisF i b smooth := hs'_smooth i } - -- Coefficient functions `g i` smooth + vanishing at x (since `X x = 0`). - let g : Fin (Module.finrank ℝ E) → M → ℝ := fun i b => + -- Coefficient functions `c i` smooth + vanishing at x (since `X x = 0`). + let c : Fin (Module.finrank ℝ E) → M → ℝ := fun i b => χ b • e.localFrame_coeff I basisF i b (X.toFun b) - have hg_smooth : ∀ i, ContMDiff I 𝓘(ℝ, ℝ) ∞ (g i) := by + have hc_smooth : ∀ i, ContMDiff I 𝓘(ℝ, ℝ) ∞ (c i) := by intro i b by_cases hb : b ∈ tsupport (χ : M → ℝ) · have hb_base : b ∈ e.baseSet := hχsupp hb @@ -758,13 +761,13 @@ theorem riemannCurvature_eq_zero_of_X_eq_zero_field filter_upwards [hχ_zero] with y hy show χ y • e.localFrame_coeff I basisF i y (X.toFun y) = 0 rw [hy, zero_smul] - have hg_zero : ∀ i, g i x = 0 := by + have hc_zero : ∀ i, c i x = 0 := by intro i show χ x • e.localFrame_coeff I basisF i x (X.toFun x) = 0 rw [hXx, map_zero, smul_zero] -- `X =ᶠ ∑ g_i • s'_i` near x. have hX_eq_sum : ∀ᶠ b in 𝓝 x, - X.toFun b = ∑ i, g i b • (s' i).toFun b := by + X.toFun b = ∑ i, c i b • (s' i).toFun b := by filter_upwards [χ.eventuallyEq_one, e.open_baseSet.mem_nhds he_mem] with b hχb hb_base show X.toFun b @@ -774,24 +777,24 @@ theorem riemannCurvature_eq_zero_of_X_eq_zero_field simp only [hχ1, one_smul] exact e.eq_sum_localFrame_coeff_smul (b := basisF) hb_base have hXsum_smooth : ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ - (fun b : M => (⟨b, ∑ i, g i b • (s' i).toFun b⟩ : TangentBundle I M)) := by + (fun b : M => (⟨b, ∑ i, c i b • (s' i).toFun b⟩ : TangentBundle I M)) := by refine ContMDiff.sum_section (s := Finset.univ) ?_ intro i _ - exact (hg_smooth i).smul_section (hs'_smooth i) + exact (hc_smooth i).smul_section (hs'_smooth i) let Xsum : SmoothVectorField I M := - { toFun := fun b => ∑ i, g i b • (s' i).toFun b + { toFun := fun b => ∑ i, c i b • (s' i).toFun b smooth := hXsum_smooth } - rw [riemannCurvature_eq_of_X_eventuallyEq X Xsum Y Z x hX_eq_sum] - show riemannCurvature HasMetric.metric (fun b => ∑ i ∈ (Finset.univ : Finset (Fin (Module.finrank ℝ E))), - g i b • (s' i).toFun b) Y.toFun Z.toFun x = 0 + rw [riemannCurvature_eq_of_X_eventuallyEq g X Xsum Y Z x hX_eq_sum] + show riemannCurvature g (fun b => ∑ i ∈ (Finset.univ : Finset (Fin (Module.finrank ℝ E))), + c i b • (s' i).toFun b) Y.toFun Z.toFun x = 0 suffices h : ∀ (T : Finset (Fin (Module.finrank ℝ E))), - riemannCurvature HasMetric.metric (fun b => ∑ i ∈ T, g i b • (s' i).toFun b) + riemannCurvature g (fun b => ∑ i ∈ T, c i b • (s' i).toFun b) Y.toFun Z.toFun x - = ∑ i ∈ T, g i x • riemannCurvature HasMetric.metric (s' i).toFun Y.toFun Z.toFun x by + = ∑ i ∈ T, c i x • riemannCurvature g (s' i).toFun Y.toFun Z.toFun x by rw [h Finset.univ] apply Finset.sum_eq_zero intro i _ - rw [hg_zero i, zero_smul] + rw [hc_zero i, zero_smul] intro T induction T using Finset.induction_on with | empty => @@ -802,73 +805,73 @@ theorem riemannCurvature_eq_zero_of_X_eq_zero_field have h_zero_pi : (fun _ : M => (0 : TangentSpace I _)) = (0 : VectorFieldSection I M) := rfl -- T1: outer cov at direction `0` = `0` (map_zero of continuous linear map in direction). - have hT1 : covDeriv HasMetric.metric (fun _ : M => (0 : TangentSpace I _)) - (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x = 0 := by - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) x) + have hT1 : covDeriv g (fun _ : M => (0 : TangentSpace I _)) + (fun y => covDeriv g Y.toFun Z.toFun y) x = 0 := by + show ((leviCivitaConnection (I := I) (M := M) g).toFun (fun y => covDeriv g Y.toFun Z.toFun y) x) ((fun _ : M => (0 : TangentSpace I _)) x) = 0 - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun _ x) (0 : TangentSpace I x) = 0 + show ((leviCivitaConnection (I := I) (M := M) g).toFun _ x) (0 : TangentSpace I x) = 0 exact map_zero _ -- Inner section `cov (fun _ => 0) Z` is the zero section. have h_inner : - (fun y => covDeriv HasMetric.metric (fun _ : M => (0 : TangentSpace I _)) Z.toFun y) + (fun y => covDeriv g (fun _ : M => (0 : TangentSpace I _)) Z.toFun y) = (fun _ : M => (0 : TangentSpace I _)) := by funext y - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun y) (0 : TangentSpace I y) = 0 + show ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun y) (0 : TangentSpace I y) = 0 exact map_zero _ -- T2: outer cov of the zero section = 0 (via `IsCovariantDerivativeOn.zero`). - have hT2 : covDeriv HasMetric.metric Y.toFun - (fun y => covDeriv HasMetric.metric (fun _ : M => (0 : TangentSpace I _)) Z.toFun y) x = 0 := by + have hT2 : covDeriv g Y.toFun + (fun y => covDeriv g (fun _ : M => (0 : TangentSpace I _)) Z.toFun y) x = 0 := by rw [h_inner] - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun (fun _ : M => (0 : TangentSpace I _)) x) (Y.toFun x) = 0 + show ((leviCivitaConnection (I := I) (M := M) g).toFun (fun _ : M => (0 : TangentSpace I _)) x) (Y.toFun x) = 0 rw [h_zero_pi] - rw [(leviCivitaConnection (I := I) (M := M) HasMetric.metric).isCovariantDerivativeOnUniv.zero (x := x)]; rfl + rw [(leviCivitaConnection (I := I) (M := M) g).isCovariantDerivativeOnUniv.zero (x := x)]; rfl -- T3: `[fun _ => 0, Y] = 0` section, then `cov 0 Z x = 0`. have h_br : VectorField.mlieBracket I (fun _ : M => (0 : TangentSpace I _)) Y.toFun = (fun _ : M => (0 : TangentSpace I _)) := by rw [h_zero_pi] exact VectorField.mlieBracket_zero_left - have hT3 : covDeriv HasMetric.metric (VectorField.mlieBracket I + have hT3 : covDeriv g (VectorField.mlieBracket I (fun _ : M => (0 : TangentSpace I _)) Y.toFun) Z.toFun x = 0 := by rw [h_br] - show ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z.toFun x) (0 : TangentSpace I x) = 0 + show ((leviCivitaConnection (I := I) (M := M) g).toFun Z.toFun x) (0 : TangentSpace I x) = 0 exact map_zero _ rw [hT1, hT2, hT3]; abel | insert j s hjs IH => - have hsplit : (fun b : M => ∑ i ∈ insert j s, g i b • (s' i).toFun b) - = ((g j • (s' j).toFun : Π b, TangentSpace I b) - + (fun b : M => ∑ i ∈ s, g i b • (s' i).toFun b)) := by + have hsplit : (fun b : M => ∑ i ∈ insert j s, c i b • (s' i).toFun b) + = ((c j • (s' j).toFun : Π b, TangentSpace I b) + + (fun b : M => ∑ i ∈ s, c i b • (s' i).toFun b)) := by funext b - change ∑ i ∈ insert j s, g i b • (s' i).toFun b - = g j b • (s' j).toFun b + ∑ i ∈ s, g i b • (s' i).toFun b + change ∑ i ∈ insert j s, c i b • (s' i).toFun b + = c j b • (s' j).toFun b + ∑ i ∈ s, c i b • (s' i).toFun b rw [Finset.sum_insert hjs] rw [hsplit] have hgj_smooth_section : ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ - (fun b : M => (⟨b, g j b • (s' j).toFun b⟩ : TangentBundle I M)) := - (hg_smooth j).smul_section (hs'_smooth j) + (fun b : M => (⟨b, c j b • (s' j).toFun b⟩ : TangentBundle I M)) := + (hc_smooth j).smul_section (hs'_smooth j) have hrest_smooth : ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ - (fun b : M => (⟨b, ∑ i ∈ s, g i b • (s' i).toFun b⟩ : TangentBundle I M)) := by + (fun b : M => (⟨b, ∑ i ∈ s, c i b • (s' i).toFun b⟩ : TangentBundle I M)) := by refine ContMDiff.sum_section (s := s) ?_ intro i _ - exact (hg_smooth i).smul_section (hs'_smooth i) + exact (hc_smooth i).smul_section (hs'_smooth i) let gjs : SmoothVectorField I M := - { toFun := fun b => g j b • (s' j).toFun b, smooth := hgj_smooth_section } + { toFun := fun b => c j b • (s' j).toFun b, smooth := hgj_smooth_section } let rest : SmoothVectorField I M := - { toFun := fun b => ∑ i ∈ s, g i b • (s' i).toFun b, smooth := hrest_smooth } - show riemannCurvature HasMetric.metric (gjs.toFun + rest.toFun) Y.toFun Z.toFun x - = ∑ i ∈ insert j s, g i x • riemannCurvature HasMetric.metric (s' i).toFun Y.toFun Z.toFun x + { toFun := fun b => ∑ i ∈ s, c i b • (s' i).toFun b, smooth := hrest_smooth } + show riemannCurvature g (gjs.toFun + rest.toFun) Y.toFun Z.toFun x + = ∑ i ∈ insert j s, c i x • riemannCurvature g (s' i).toFun Y.toFun Z.toFun x have h_add : - riemannCurvature HasMetric.metric (gjs.toFun + rest.toFun) Y.toFun Z.toFun x - = riemannCurvature HasMetric.metric gjs.toFun Y.toFun Z.toFun x - + riemannCurvature HasMetric.metric rest.toFun Y.toFun Z.toFun x := by - have := riemannCurvature_add_first gjs rest Y Z x + riemannCurvature g (gjs.toFun + rest.toFun) Y.toFun Z.toFun x + = riemannCurvature g gjs.toFun Y.toFun Z.toFun x + + riemannCurvature g rest.toFun Y.toFun Z.toFun x := by + have := riemannCurvature_add_first g gjs rest Y Z x simpa using this have h_smul : - riemannCurvature HasMetric.metric gjs.toFun Y.toFun Z.toFun x - = g j x • riemannCurvature HasMetric.metric (s' j).toFun Y.toFun Z.toFun x := by - show riemannCurvature HasMetric.metric (g j • (s' j).toFun) Y.toFun Z.toFun x - = g j x • riemannCurvature HasMetric.metric (s' j).toFun Y.toFun Z.toFun x + riemannCurvature g gjs.toFun Y.toFun Z.toFun x + = c j x • riemannCurvature g (s' j).toFun Y.toFun Z.toFun x := by + show riemannCurvature g (c j • (s' j).toFun) Y.toFun Z.toFun x + = c j x • riemannCurvature g (s' j).toFun Y.toFun Z.toFun x exact riemannCurvature_smul_first_scalar_field - (g j) (s' j) Y Z x (hg_smooth j) + g (c j) (s' j) Y Z x (hc_smooth j) rw [h_add, h_smul, IH, Finset.sum_insert hjs] /-- **Math.** **X-slot pointwise dependence**: `X x = X' x ⇒ R(X, Y) Z(x) = R(X', Y) Z(x)`. -/ @@ -876,19 +879,19 @@ theorem riemannCurvature_eq_of_X_eq_at [IsManifold I 2 M] [T2Space M] (X X' Y Z : SmoothVectorField I M) (x : M) (hXX' : X.toFun x = X'.toFun x) : - riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x - = riemannCurvature HasMetric.metric X'.toFun Y.toFun Z.toFun x := by + riemannCurvature g X.toFun Y.toFun Z.toFun x + = riemannCurvature g X'.toFun Y.toFun Z.toFun x := by let τ : SmoothVectorField I M := X - X' have hτ_zero : τ.toFun x = 0 := by show X.toFun x - X'.toFun x = 0 rw [hXX']; abel - have hτ_vanish : riemannCurvature HasMetric.metric τ.toFun Y.toFun Z.toFun x = 0 := - riemannCurvature_eq_zero_of_X_eq_zero_field τ Y Z x hτ_zero + have hτ_vanish : riemannCurvature g τ.toFun Y.toFun Z.toFun x = 0 := + riemannCurvature_eq_zero_of_X_eq_zero_field g τ Y Z x hτ_zero have h_pi : (X' + τ).toFun = X.toFun := by funext y show X'.toFun y + (X.toFun y - X'.toFun y) = X.toFun y abel - have h_add := riemannCurvature_add_first X' τ Y Z x + have h_add := riemannCurvature_add_first g X' τ Y Z x rw [h_pi] at h_add rw [h_add, hτ_vanish, add_zero] @@ -898,19 +901,19 @@ theorem riemannCurvature_eq_of_Y_eq_at [IsManifold I 2 M] [T2Space M] (X Y Y' Z : SmoothVectorField I M) (x : M) (hYY' : Y.toFun x = Y'.toFun x) : - riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x - = riemannCurvature HasMetric.metric X.toFun Y'.toFun Z.toFun x := by + riemannCurvature g X.toFun Y.toFun Z.toFun x + = riemannCurvature g X.toFun Y'.toFun Z.toFun x := by -- R(X, Y) Z x = -R(Y, X) Z x = -R(Y', X) Z x = R(X, Y') Z x. - rw [riemannCurvature_antisymm X.toFun Y.toFun Z.toFun x, - riemannCurvature_eq_of_X_eq_at Y Y' X Z x hYY', - ← riemannCurvature_antisymm X.toFun Y'.toFun Z.toFun x] + rw [riemannCurvature_antisymm g X.toFun Y.toFun Z.toFun x, + riemannCurvature_eq_of_X_eq_at g Y Y' X Z x hYY', + ← riemannCurvature_antisymm g X.toFun Y'.toFun Z.toFun x] -/-- **Math.** **Pointwise well-definedness of `riemannCurvature HasMetric.metric` on smooth global sections**: +/-- **Math.** **Pointwise well-definedness of `riemannCurvature g` on smooth global sections**: given two triples `(X, Y, Z)` and `(X', Y', Z')` of smooth global sections -agreeing pointwise at `x`, the values of `riemannCurvature HasMetric.metric` at `x` coincide. +agreeing pointwise at `x`, the values of `riemannCurvature g` at `x` coincide. Chained through the X-, Y-, and Z-slot `eq_at` lemmas. Used to define -`riemannCurvature HasMetric.metric` as a continuous trilinear form `riemannOp x` on +`riemannCurvature g` as a continuous trilinear form `riemannOp x` on `T_xM × T_xM × T_xM → T_xM` (downstream bundling). -/ theorem riemannCurvature_eq_of_pointwise_eq [IsManifold I 2 M] [T2Space M] @@ -919,10 +922,10 @@ theorem riemannCurvature_eq_of_pointwise_eq (hX_eq : X.toFun x = X'.toFun x) (hY_eq : Y.toFun x = Y'.toFun x) (hZ_eq : Z.toFun x = Z'.toFun x) : - riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x - = riemannCurvature HasMetric.metric X'.toFun Y'.toFun Z'.toFun x := by - rw [riemannCurvature_eq_of_X_eq_at X X' Y Z x hX_eq, - riemannCurvature_eq_of_Y_eq_at X' Y Y' Z x hY_eq, - riemannCurvature_eq_of_Z_eq_at X' Y' Z Z' x h_interior hZ_eq] + riemannCurvature g X.toFun Y.toFun Z.toFun x + = riemannCurvature g X'.toFun Y'.toFun Z'.toFun x := by + rw [riemannCurvature_eq_of_X_eq_at g X X' Y Z x hX_eq, + riemannCurvature_eq_of_Y_eq_at g X' Y Y' Z x hY_eq, + riemannCurvature_eq_of_Z_eq_at g X' Y' Z Z' x h_interior hZ_eq] end Riemannian diff --git a/OpenGALib/Riemannian/Operators/Bochner.lean b/OpenGALib/Riemannian/Operators/Bochner.lean index 94bf821..7765c68 100644 --- a/OpenGALib/Riemannian/Operators/Bochner.lean +++ b/OpenGALib/Riemannian/Operators/Bochner.lean @@ -99,7 +99,12 @@ theorem bochner_leibniz_trace_reduction (covDeriv HasMetric.metric (Bi i).toFun (manifoldGradient (I := I) HasMetric.metric f) x) (covDeriv HasMetric.metric (Bi i).toFun (manifoldGradient (I := I) HasMetric.metric f) x) := by intro i - rw [hessian_gradientNormSq_apply_section f (Bi i) x h_grad] + show (1 / 2 : ℝ) * hessian (I := I) (M := M) HasMetric.metric + (fun y => HasMetric.metric.metricInner y + (manifoldGradient (I := I) HasMetric.metric f y) + (manifoldGradient (I := I) HasMetric.metric f y)) + (Bi i).toFun (Bi i).toFun x = _ + rw [hessian_gradientNormSq_apply_section HasMetric.metric f (Bi i) x h_grad] ring rw [Finset.sum_congr rfl (fun i _ => h_summand i), Finset.sum_add_distrib] -- Step 3: identify the two sums. @@ -204,6 +209,20 @@ theorem bochner_leibniz_trace_reduction _ = ∑ j, ⟪v, b j⟫_ℝ ^ 2 := (b.sum_sq_inner_left v).symm _ = ∑ j, (metricInner x v (b j)) ^ 2 := rfl +/-- **Math.** **Explicit-`g` form of the Leibniz trace reduction**. -/ +theorem bochner_leibniz_trace_reduction_g + [IsManifold I 2 M] + (g : RiemannianMetric I M) (hg : g = hm.metric) + (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) : + (1 / 2 : ℝ) * Operators.scalarLaplacian g + (fun y => g.metricInner y (manifoldGradient (I := I) g f y) + (manifoldGradient (I := I) g f y)) x + = g.metricInner x (connectionLaplacian g (manifoldGradient (I := I) g f) x) + (manifoldGradient (I := I) g f x) + + Operators.frobeniusSq (I := I) (M := M) (Operators.hessianBilin (I := I) g f) x := by + subst hg + exact bochner_leibniz_trace_reduction f hf x + /-! ## The headline identity -/ /-- **Math.** **Bochner–Weitzenböck identity** (unconditional under @@ -228,5 +247,25 @@ theorem bochner_weitzenboeck bochner_connectionLaplacian_grad_decomposition f hf x] abel +/-- **Math.** **Explicit-`g` form of the Bochner–Weitzenböck identity**. +Same statement as `bochner_weitzenboeck` but the metric `g` is an explicit +`RiemannianMetric I M` parameter constrained by `hg : g = hm.metric`, +giving consumers a `g`-parametric API without changing the underlying +proof. Discharged via `subst hg` and `bochner_weitzenboeck`. -/ +theorem bochner_weitzenboeck_g + [IsManifold I 2 M] + (g : RiemannianMetric I M) (hg : g = hm.metric) + (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) : + (1 / 2 : ℝ) * Operators.scalarLaplacian g + (fun y => g.metricInner y (manifoldGradient (I := I) g f y) + (manifoldGradient (I := I) g f y)) x = + Operators.frobeniusSq (I := I) (M := M) (Operators.hessianBilin (I := I) g f) x + + g.metricInner x (manifoldGradient (I := I) g f x) + (manifoldGradient (I := I) g (Operators.scalarLaplacian g f) x) + + ricciTensor g x (manifoldGradient (I := I) g f x) + (manifoldGradient (I := I) g f x) := by + subst hg + exact bochner_weitzenboeck f hf x + end Operators end Riemannian diff --git a/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean b/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean index bdf12c1..19265eb 100644 --- a/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean +++ b/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean @@ -389,7 +389,7 @@ theorem heart_curvature_orthonormal_sum_eq_ricci = riemannCurvature HasMetric.metric (fun _ : M => ((Bi i).toFun x : TangentSpace I x)) WV.toFun GV.toFun x - exact riemannCurvature_eq_of_pointwise_eq + exact riemannCurvature_eq_of_pointwise_eq HasMetric.metric (Bi i) (SmoothVectorField.const ((Bi i).toFun x : E)) W WV gradF GV x h_interior rfl rfl rfl rw [hR_eq]; rfl diff --git a/OpenGALib/Riemannian/Operators/Bochner/HessianExpansion.lean b/OpenGALib/Riemannian/Operators/Bochner/HessianExpansion.lean index 5e98cac..101341a 100644 --- a/OpenGALib/Riemannian/Operators/Bochner/HessianExpansion.lean +++ b/OpenGALib/Riemannian/Operators/Bochner/HessianExpansion.lean @@ -41,6 +41,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpa {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] [T2Space M] [IsLocallyConstantChartedSpace H M] [hm : HasMetric I M] + (g : RiemannianMetric I M) /-! ## Helpers for the Leibniz trace reduction (E) -/ @@ -48,49 +49,49 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpa Metric-compatibility on $(\nabla f, \nabla f)$ plus inner-product symmetry. -/ theorem mfderiv_gradientNormSq_apply (f : M → ℝ) (y : M) (v : TangentSpace I y) - (h_grad_y : TangentSmoothAt (manifoldGradient (I := I) HasMetric.metric f) y) : - mfderiv I 𝓘(ℝ, ℝ) (‖grad_g[I] f‖²_g) y v - = 2 * metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y v) - (manifoldGradient (I := I) HasMetric.metric f y) := by + (h_grad_y : TangentSmoothAt (manifoldGradient (I := I) g f) y) : + mfderiv I 𝓘(ℝ, ℝ) ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) y v + = 2 * g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y v) + (manifoldGradient (I := I) g f y) := by show mfderiv I 𝓘(ℝ, ℝ) - (fun z : M => metricInner z (manifoldGradient (I := I) HasMetric.metric f z) - (manifoldGradient (I := I) HasMetric.metric f z)) y v = _ + (fun z : M => g.metricInner z (manifoldGradient (I := I) g f z) + (manifoldGradient (I := I) g f z)) y v = _ have hVsm : TangentSmoothAt (fun _ : M => (v : TangentSpace I y)) y := (SmoothVectorField.const (I := I) (M := M) (v : E)).smoothAt y - -- Bridge metric-compat ∇ → `.toFun` form for the subsequent `rw [h, metricInner_comm ...]`. - have h := leviCivitaConnection_metric_compatible HasMetric.metric + -- Bridge metric-compat ∇ → `.toFun` form for the subsequent `rw [h, g.metricInner_comm ...]`. + have h := leviCivitaConnection_metric_compatible g (fun _ : M => (v : TangentSpace I y)) - (manifoldGradient (I := I) HasMetric.metric f) - (manifoldGradient (I := I) HasMetric.metric f) + (manifoldGradient (I := I) g f) + (manifoldGradient (I := I) g f) y hVsm h_grad_y h_grad_y simp only [← leviCivitaConnection_toFun_eq_covDeriv] at h - -- Cast h to typeclass `metricInner` abbrev form for rw matching. - change ((mfderiv% fun y' => metricInner y' (manifoldGradient (I := I) HasMetric.metric f y') - (manifoldGradient (I := I) HasMetric.metric f y')) y) v - = metricInner y - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (manifoldGradient (I := I) HasMetric.metric f) y v) - (manifoldGradient (I := I) HasMetric.metric f y) - + metricInner y (manifoldGradient (I := I) HasMetric.metric f y) - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (manifoldGradient (I := I) HasMetric.metric f) y v) at h - rw [h, metricInner_comm y (manifoldGradient (I := I) HasMetric.metric f y) - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (manifoldGradient (I := I) HasMetric.metric f) y v)] - -- `covDerivAt HasMetric.metric Y x = lcc.toFun Y x` def-eq; close `a + a = 2 * a` via ring after `show`. - show metricInner y - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (manifoldGradient (I := I) HasMetric.metric f) y v) - (manifoldGradient (I := I) HasMetric.metric f y) - + metricInner y - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (manifoldGradient (I := I) HasMetric.metric f) y v) - (manifoldGradient (I := I) HasMetric.metric f y) - = 2 * metricInner y - ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (manifoldGradient (I := I) HasMetric.metric f) y v) - (manifoldGradient (I := I) HasMetric.metric f y) + -- Cast h to typeclass `g.metricInner` abbrev form for rw matching. + change ((mfderiv% fun y' => g.metricInner y' (manifoldGradient (I := I) g f y') + (manifoldGradient (I := I) g f y')) y) v + = g.metricInner y + ((leviCivitaConnection (I := I) (M := M) g).toFun + (manifoldGradient (I := I) g f) y v) + (manifoldGradient (I := I) g f y) + + g.metricInner y (manifoldGradient (I := I) g f y) + ((leviCivitaConnection (I := I) (M := M) g).toFun + (manifoldGradient (I := I) g f) y v) at h + rw [h, g.metricInner_comm y (manifoldGradient (I := I) g f y) + ((leviCivitaConnection (I := I) (M := M) g).toFun + (manifoldGradient (I := I) g f) y v)] + -- `covDerivAt g Y x = lcc.toFun Y x` def-eq; close `a + a = 2 * a` via ring after `show`. + show g.metricInner y + ((leviCivitaConnection (I := I) (M := M) g).toFun + (manifoldGradient (I := I) g f) y v) + (manifoldGradient (I := I) g f y) + + g.metricInner y + ((leviCivitaConnection (I := I) (M := M) g).toFun + (manifoldGradient (I := I) g f) y v) + (manifoldGradient (I := I) g f y) + = 2 * g.metricInner y + ((leviCivitaConnection (I := I) (M := M) g).toFun + (manifoldGradient (I := I) g f) y v) + (manifoldGradient (I := I) g f y) ring /-- **Math.** **Section-form Hessian expansion** of $g = |\nabla f|_g^2$ @@ -103,135 +104,135 @@ theorem hessian_gradientNormSq_apply_section [IsManifold I 2 M] (f : M → ℝ) (B : SmoothVectorField I M) (x : M) (h_grad : ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ - (fun y => (⟨y, manifoldGradient (I := I) HasMetric.metric f y⟩ : TangentBundle I M))) : - hessian (I := I) (M := M) HasMetric.metric (‖grad_g[I] f‖²_g) B.toFun B.toFun x - = 2 * (metricInner x - (secondCovDerivSection (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) B.toFun B.toFun x) - (manifoldGradient (I := I) HasMetric.metric f x) - + metricInner x - (covDeriv HasMetric.metric B.toFun (manifoldGradient (I := I) HasMetric.metric f) x) - (covDeriv HasMetric.metric B.toFun (manifoldGradient (I := I) HasMetric.metric f) x)) := by + (fun y => (⟨y, manifoldGradient (I := I) g f y⟩ : TangentBundle I M))) : + hessian (I := I) (M := M) g ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) B.toFun B.toFun x + = 2 * (g.metricInner x + (secondCovDerivSection (I := I) (M := M) g (manifoldGradient (I := I) g f) B.toFun B.toFun x) + (manifoldGradient (I := I) g f x) + + g.metricInner x + (covDeriv g B.toFun (manifoldGradient (I := I) g f) x) + (covDeriv g B.toFun (manifoldGradient (I := I) g f) x)) := by classical - let gradF : SmoothVectorField I M := ⟨manifoldGradient (I := I) HasMetric.metric f, h_grad⟩ - have h_grad_smoothAt : ∀ y, TangentSmoothAt (manifoldGradient (I := I) HasMetric.metric f) y := + let gradF : SmoothVectorField I M := ⟨manifoldGradient (I := I) g f, h_grad⟩ + have h_grad_smoothAt : ∀ y, TangentSmoothAt (manifoldGradient (I := I) g f) y := fun y => gradF.smoothAt y - have hg_smooth : ContMDiff I 𝓘(ℝ, ℝ) ∞ ((‖grad_g[I] f‖²_g) : M → ℝ) := by + have hg_smooth : ContMDiff I 𝓘(ℝ, ℝ) ∞ (((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) : M → ℝ) := by show ContMDiff I 𝓘(ℝ, ℝ) ∞ - (fun y => metricInner y (manifoldGradient (I := I) HasMetric.metric f y) - (manifoldGradient (I := I) HasMetric.metric f y)) - exact metricInner_contMDiff h_grad h_grad + (fun y => g.metricInner y (manifoldGradient (I := I) g f y) + (manifoldGradient (I := I) g f y)) + exact g.metricInner_contMDiff h_grad h_grad have h_grad_g_cmd : ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ - (fun y => (⟨y, manifoldGradient (I := I) HasMetric.metric (‖grad_g[I] f‖²_g) y⟩ + (fun y => (⟨y, manifoldGradient (I := I) g ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) y⟩ : TangentBundle I M)) := - Riemannian.manifoldGradient_smooth_of_smooth HasMetric.metric (‖grad_g[I] f‖²_g) hg_smooth + Riemannian.manifoldGradient_smooth_of_smooth g ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) hg_smooth have h_grad_g_smoothAt : - TangentSmoothAt (manifoldGradient (I := I) HasMetric.metric (‖grad_g[I] f‖²_g)) x := + TangentSmoothAt (manifoldGradient (I := I) g ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y)))) x := TangentSmoothAt.mk (h_grad_g_cmd.mdifferentiableAt (by simp : (∞ : ℕ∞ω) ≠ 0)) have hBsm : TangentSmoothAt B.toFun x := B.smoothAt x - -- C² gap on ∇f: smoothness of `y ↦ covDerivAt HasMetric.metric ∇f y (B y)` at x + -- C² gap on ∇f: smoothness of `y ↦ covDerivAt g ∇f y (B y)` at x -- (smooth-direction case via `leviCivitaConnection_smoothAt_smoothVF_dir`). have hBnf_smooth : TangentSmoothAt (fun y : M => - (leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (manifoldGradient (I := I) HasMetric.metric f) y (B.toFun y)) x := - leviCivitaConnection_smoothAt_smoothVF_dir HasMetric.metric B gradF x + (leviCivitaConnection (I := I) (M := M) g).toFun + (manifoldGradient (I := I) g f) y (B.toFun y)) x := + leviCivitaConnection_smoothAt_smoothVF_dir g B gradF x -- Level-1 bridge: hessian = iterated mDirDeriv minus Christoffel correction. - have h_bridge := Riemannian.Operators.hessian_eq_mDirDeriv_iterate_sub_chris HasMetric.metric - (‖grad_g[I] f‖²_g) B.toFun B.toFun x + have h_bridge := Riemannian.Operators.hessian_eq_mDirDeriv_iterate_sub_chris g + ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) B.toFun B.toFun x h_grad_g_smoothAt hBsm hBsm -- mDirDeriv (|∇f|²) y (B y) = 2 g(∇_{B y} ∇f, ∇f) y (via `mfderiv_gradientNormSq_apply`). have h_inner_eq : - (fun y : M => mDirDeriv (I := I) (‖grad_g[I] f‖²_g) y (B.toFun y)) - = (fun y : M => 2 * metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (B.toFun y)) - (manifoldGradient (I := I) HasMetric.metric f y)) := by - funext y; exact mfderiv_gradientNormSq_apply f y (B.toFun y) (h_grad_smoothAt y) + (fun y : M => mDirDeriv (I := I) ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) y (B.toFun y)) + = (fun y : M => 2 * g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (B.toFun y)) + (manifoldGradient (I := I) g f y)) := by + funext y; exact mfderiv_gradientNormSq_apply g f y (B.toFun y) (h_grad_smoothAt y) rw [h_inner_eq] at h_bridge -- Christoffel term: mDirDeriv (|∇f|²) x (∇_B B x) = 2 g(∇_{∇_B B x} ∇f, ∇f x). - have h_chris_term : mDirDeriv (I := I) (‖grad_g[I] f‖²_g) x - (covDeriv HasMetric.metric B.toFun B.toFun x) - = 2 * metricInner x - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x - (covDeriv HasMetric.metric B.toFun B.toFun x)) - (manifoldGradient (I := I) HasMetric.metric f x) := - mfderiv_gradientNormSq_apply f x (covDeriv HasMetric.metric B.toFun B.toFun x) + have h_chris_term : mDirDeriv (I := I) ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) x + (covDeriv g B.toFun B.toFun x) + = 2 * g.metricInner x + (covDerivAt g (manifoldGradient (I := I) g f) x + (covDeriv g B.toFun B.toFun x)) + (manifoldGradient (I := I) g f x) := + mfderiv_gradientNormSq_apply g f x (covDeriv g B.toFun B.toFun x) (h_grad_smoothAt x) rw [h_chris_term] at h_bridge -- Pull `2` out of the outer mDirDeriv via `const_smul_mfderiv`. have h_inner_smooth : MDifferentiableAt I 𝓘(ℝ, ℝ) - (fun y : M => metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (B.toFun y)) - (manifoldGradient (I := I) HasMetric.metric f y)) x := - metricInner_mdifferentiableAt_of_tangentSmoothAt hBnf_smooth (h_grad_smoothAt x) + (fun y : M => g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (B.toFun y)) + (manifoldGradient (I := I) g f y)) x := + g.metricInner_mdifferentiableAt_of_tangentSmoothAt hBnf_smooth (h_grad_smoothAt x) have h_pull_two : mDirDeriv (I := I) - (fun y : M => 2 * metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (B.toFun y)) - (manifoldGradient (I := I) HasMetric.metric f y)) x (B.toFun x) + (fun y : M => 2 * g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (B.toFun y)) + (manifoldGradient (I := I) g f y)) x (B.toFun x) = 2 * mDirDeriv (I := I) - (fun y : M => metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (B.toFun y)) - (manifoldGradient (I := I) HasMetric.metric f y)) x (B.toFun x) := by + (fun y : M => g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (B.toFun y)) + (manifoldGradient (I := I) g f y)) x (B.toFun x) := by show mfderiv I 𝓘(ℝ, ℝ) - (fun y : M => 2 * metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (B.toFun y)) - (manifoldGradient (I := I) HasMetric.metric f y)) x (B.toFun x) = _ - have h_smul : (fun y : M => 2 * metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (B.toFun y)) - (manifoldGradient (I := I) HasMetric.metric f y)) - = (2 : ℝ) • (fun y : M => metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (B.toFun y)) - (manifoldGradient (I := I) HasMetric.metric f y)) := by + (fun y : M => 2 * g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (B.toFun y)) + (manifoldGradient (I := I) g f y)) x (B.toFun x) = _ + have h_smul : (fun y : M => 2 * g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (B.toFun y)) + (manifoldGradient (I := I) g f y)) + = (2 : ℝ) • (fun y : M => g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (B.toFun y)) + (manifoldGradient (I := I) g f y)) := by funext y; simp [Pi.smul_apply, smul_eq_mul] rw [h_smul, const_smul_mfderiv h_inner_smooth (2 : ℝ)] rfl rw [h_pull_two] at h_bridge - -- Level-2 metric-compat on (B, ∇_B ∇f, ∇f) at x; converts to covDerivAt HasMetric.metric form. - have h_compat2 := leviCivitaConnection_metric_compatible HasMetric.metric + -- Level-2 metric-compat on (B, ∇_B ∇f, ∇f) at x; converts to covDerivAt g form. + have h_compat2 := leviCivitaConnection_metric_compatible g B.toFun (fun y : M => - (leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (manifoldGradient (I := I) HasMetric.metric f) y (B.toFun y)) - (manifoldGradient (I := I) HasMetric.metric f) x hBsm hBnf_smooth (h_grad_smoothAt x) + (leviCivitaConnection (I := I) (M := M) g).toFun + (manifoldGradient (I := I) g f) y (B.toFun y)) + (manifoldGradient (I := I) g f) x hBsm hBnf_smooth (h_grad_smoothAt x) change mDirDeriv (I := I) - (fun y : M => metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (B.toFun y)) - (manifoldGradient (I := I) HasMetric.metric f y)) x (B.toFun x) - = metricInner x - (covDerivAt HasMetric.metric + (fun y : M => g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (B.toFun y)) + (manifoldGradient (I := I) g f y)) x (B.toFun x) + = g.metricInner x + (covDerivAt g (fun y : M => - covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (B.toFun y)) + covDerivAt g (manifoldGradient (I := I) g f) y (B.toFun y)) x (B.toFun x)) - (manifoldGradient (I := I) HasMetric.metric f x) - + metricInner x - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x (B.toFun x)) - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x (B.toFun x)) + (manifoldGradient (I := I) g f x) + + g.metricInner x + (covDerivAt g (manifoldGradient (I := I) g f) x (B.toFun x)) + (covDerivAt g (manifoldGradient (I := I) g f) x (B.toFun x)) at h_compat2 rw [h_compat2] at h_bridge -- Connect to `secondCovDerivSection`: `(∇^2 ∇f)(B, B) x = ∇_B (∇_B ∇f) x - ∇_{∇_B B x} ∇f`. have h_secondCDS : - metricInner x - (secondCovDerivSection (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) B.toFun B.toFun x) - (manifoldGradient (I := I) HasMetric.metric f x) - = metricInner x - (covDerivAt HasMetric.metric + g.metricInner x + (secondCovDerivSection (I := I) (M := M) g (manifoldGradient (I := I) g f) B.toFun B.toFun x) + (manifoldGradient (I := I) g f x) + = g.metricInner x + (covDerivAt g (fun y : M => - covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (B.toFun y)) + covDerivAt g (manifoldGradient (I := I) g f) y (B.toFun y)) x (B.toFun x)) - (manifoldGradient (I := I) HasMetric.metric f x) - - metricInner x - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x - (covDeriv HasMetric.metric B.toFun B.toFun x)) - (manifoldGradient (I := I) HasMetric.metric f x) := by + (manifoldGradient (I := I) g f x) + - g.metricInner x + (covDerivAt g (manifoldGradient (I := I) g f) x + (covDeriv g B.toFun B.toFun x)) + (manifoldGradient (I := I) g f x) := by unfold secondCovDerivSection - rw [metricInner_sub_left] + rw [g.metricInner_sub_left] rfl - -- `covDeriv HasMetric.metric B.toFun ∇f x = covDerivAt HasMetric.metric ∇f x (B x)` (def). + -- `covDeriv g B.toFun ∇f x = covDerivAt g ∇f x (B x)` (def). have h_covDeriv_eq : - covDeriv HasMetric.metric B.toFun (manifoldGradient (I := I) HasMetric.metric f) x - = covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x (B.toFun x) := rfl + covDeriv g B.toFun (manifoldGradient (I := I) g f) x + = covDerivAt g (manifoldGradient (I := I) g f) x (B.toFun x) := rfl -- Combine: linearly relate `h_bridge` to the goal. rw [h_covDeriv_eq] linarith [h_bridge, h_secondCDS] @@ -246,160 +247,160 @@ theorem hessian_gradientNormSq_apply_chartFrame [IsManifold I 2 M] (f : M → ℝ) (x : M) (v : TangentSpace I x) (h_grad : ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ - (fun y => (⟨y, manifoldGradient (I := I) HasMetric.metric f y⟩ : TangentBundle I M))) : - hessian (I := I) (M := M) HasMetric.metric (‖grad_g[I] f‖²_g) + (fun y => (⟨y, manifoldGradient (I := I) g f y⟩ : TangentBundle I M))) : + hessian (I := I) (M := M) g ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) (fun _ : M => (v : TangentSpace I x)) (fun _ : M => (v : TangentSpace I x)) x - = 2 * (metricInner x - (secondCovDerivAt (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x v v) - (manifoldGradient (I := I) HasMetric.metric f x) - + metricInner x - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x v) - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x v)) := by - let gradSV : SmoothVectorField I M := ⟨manifoldGradient (I := I) HasMetric.metric f, h_grad⟩ - have h_grad_smoothAt : ∀ y, TangentSmoothAt (manifoldGradient (I := I) HasMetric.metric f) y := + = 2 * (g.metricInner x + (secondCovDerivAt (I := I) (M := M) g (manifoldGradient (I := I) g f) x v v) + (manifoldGradient (I := I) g f x) + + g.metricInner x + (covDerivAt g (manifoldGradient (I := I) g f) x v) + (covDerivAt g (manifoldGradient (I := I) g f) x v)) := by + let gradSV : SmoothVectorField I M := ⟨manifoldGradient (I := I) g f, h_grad⟩ + have h_grad_smoothAt : ∀ y, TangentSmoothAt (manifoldGradient (I := I) g f) y := fun y => gradSV.smoothAt y - have hg_smooth : ContMDiff I 𝓘(ℝ, ℝ) ∞ ((‖grad_g[I] f‖²_g) : M → ℝ) := by + have hg_smooth : ContMDiff I 𝓘(ℝ, ℝ) ∞ (((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) : M → ℝ) := by show ContMDiff I 𝓘(ℝ, ℝ) ∞ - (fun y => metricInner y (manifoldGradient (I := I) HasMetric.metric f y) - (manifoldGradient (I := I) HasMetric.metric f y)) - exact metricInner_contMDiff h_grad h_grad + (fun y => g.metricInner y (manifoldGradient (I := I) g f y) + (manifoldGradient (I := I) g f y)) + exact g.metricInner_contMDiff h_grad h_grad have h_grad_g_cmd : ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ - (fun y => (⟨y, manifoldGradient (I := I) HasMetric.metric (‖grad_g[I] f‖²_g) y⟩ + (fun y => (⟨y, manifoldGradient (I := I) g ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) y⟩ : TangentBundle I M)) := - Riemannian.manifoldGradient_smooth_of_smooth HasMetric.metric (‖grad_g[I] f‖²_g) hg_smooth + Riemannian.manifoldGradient_smooth_of_smooth g ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) hg_smooth have h_grad_g_smoothAt : - TangentSmoothAt (manifoldGradient (I := I) HasMetric.metric (‖grad_g[I] f‖²_g)) x := + TangentSmoothAt (manifoldGradient (I := I) g ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y)))) x := TangentSmoothAt.mk (h_grad_g_cmd.mdifferentiableAt (by simp : (∞ : ℕ∞ω) ≠ 0)) have hVsm : TangentSmoothAt (fun _ : M => (v : TangentSpace I x)) x := (SmoothVectorField.const (I := I) (M := M) (v : E)).smoothAt x - -- C² gap on ∇f: smoothness of `y ↦ covDerivAt HasMetric.metric ∇f y v` at x. + -- C² gap on ∇f: smoothness of `y ↦ covDerivAt g ∇f y v` at x. have hSvsm : TangentSmoothAt (fun y : M => - (leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) x := - leviCivitaConnection_smoothAt_smoothVF_dir HasMetric.metric + (leviCivitaConnection (I := I) (M := M) g).toFun + (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) x := + leviCivitaConnection_smoothAt_smoothVF_dir g (SmoothVectorField.const (I := I) (M := M) (v : E)) gradSV x - have h_bridge := Riemannian.Operators.hessian_eq_mDirDeriv_iterate_sub_chris HasMetric.metric - (‖grad_g[I] f‖²_g) (fun _ : M => (v : TangentSpace I x)) + have h_bridge := Riemannian.Operators.hessian_eq_mDirDeriv_iterate_sub_chris g + ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) (fun _ : M => (v : TangentSpace I x)) (fun _ : M => (v : TangentSpace I x)) x h_grad_g_smoothAt hVsm hVsm have h_inner_eq : - (fun y : M => mDirDeriv (I := I) (‖grad_g[I] f‖²_g) y (v : TangentSpace I x)) - = (fun y : M => 2 * metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f y)) := by - funext y; exact mfderiv_gradientNormSq_apply f y v (h_grad_smoothAt y) + (fun y : M => mDirDeriv (I := I) ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) y (v : TangentSpace I x)) + = (fun y : M => 2 * g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) + (manifoldGradient (I := I) g f y)) := by + funext y; exact mfderiv_gradientNormSq_apply g f y v (h_grad_smoothAt y) rw [h_inner_eq] at h_bridge - have h_chris_term : mDirDeriv (I := I) (‖grad_g[I] f‖²_g) x - (covDeriv HasMetric.metric (fun _ : M => (v : TangentSpace I x)) + have h_chris_term : mDirDeriv (I := I) ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) x + (covDeriv g (fun _ : M => (v : TangentSpace I x)) (fun _ : M => (v : TangentSpace I x)) x) - = 2 * metricInner x - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x - (covDeriv HasMetric.metric (fun _ : M => (v : TangentSpace I x)) + = 2 * g.metricInner x + (covDerivAt g (manifoldGradient (I := I) g f) x + (covDeriv g (fun _ : M => (v : TangentSpace I x)) (fun _ : M => (v : TangentSpace I x)) x)) - (manifoldGradient (I := I) HasMetric.metric f x) := - mfderiv_gradientNormSq_apply f x - (covDeriv HasMetric.metric (fun _ : M => (v : TangentSpace I x)) + (manifoldGradient (I := I) g f x) := + mfderiv_gradientNormSq_apply g f x + (covDeriv g (fun _ : M => (v : TangentSpace I x)) (fun _ : M => (v : TangentSpace I x)) x) (h_grad_smoothAt x) rw [h_chris_term] at h_bridge have h_inner_smooth : MDifferentiableAt I 𝓘(ℝ, ℝ) - (fun y : M => metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f y)) x := - metricInner_mdifferentiableAt_of_tangentSmoothAt hSvsm (h_grad_smoothAt x) + (fun y : M => g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) + (manifoldGradient (I := I) g f y)) x := + g.metricInner_mdifferentiableAt_of_tangentSmoothAt hSvsm (h_grad_smoothAt x) -- Pull `2` out of the iterated `mDirDeriv` via `const_smul_mfderiv`. have h_pull_two : mDirDeriv (I := I) - (fun y : M => 2 * metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f y)) x v + (fun y : M => 2 * g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) + (manifoldGradient (I := I) g f y)) x v = 2 * mDirDeriv (I := I) - (fun y : M => metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f y)) x v := by + (fun y : M => g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) + (manifoldGradient (I := I) g f y)) x v := by show mfderiv I 𝓘(ℝ, ℝ) - (fun y : M => 2 * metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f y)) x v = _ - have h_smul : (fun y : M => 2 * metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f y)) - = (2 : ℝ) • (fun y : M => metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f y)) := by + (fun y : M => 2 * g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) + (manifoldGradient (I := I) g f y)) x v = _ + have h_smul : (fun y : M => 2 * g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) + (manifoldGradient (I := I) g f y)) + = (2 : ℝ) • (fun y : M => g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) + (manifoldGradient (I := I) g f y)) := by funext y; simp [Pi.smul_apply, smul_eq_mul] rw [h_smul, const_smul_mfderiv h_inner_smooth (2 : ℝ)] - show (2 : ℝ) • (mfderiv I 𝓘(ℝ, ℝ) (fun y : M => metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f y)) x) v - = 2 * mDirDeriv (I := I) (fun y : M => metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f y)) x v + show (2 : ℝ) • (mfderiv I 𝓘(ℝ, ℝ) (fun y : M => g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) + (manifoldGradient (I := I) g f y)) x) v + = 2 * mDirDeriv (I := I) (fun y : M => g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) + (manifoldGradient (I := I) g f y)) x v rfl rw [h_pull_two] at h_bridge - -- Level-2 metric-compat on (const v, S_v, ∇f); convert lcc.toFun to covDerivAt HasMetric.metric + -- Level-2 metric-compat on (const v, S_v, ∇f); convert lcc.toFun to covDerivAt g -- (def-eq) at h_compat2 to match h_bridge's pattern. - have h_compat2 := leviCivitaConnection_metric_compatible HasMetric.metric + have h_compat2 := leviCivitaConnection_metric_compatible g (fun _ : M => (v : TangentSpace I x)) (fun y : M => - (leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun - (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f) x hVsm hSvsm (h_grad_smoothAt x) + (leviCivitaConnection (I := I) (M := M) g).toFun + (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) + (manifoldGradient (I := I) g f) x hVsm hSvsm (h_grad_smoothAt x) change mDirDeriv (I := I) - (fun y : M => metricInner y - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f y)) x v - = metricInner x - (covDerivAt HasMetric.metric + (fun y : M => g.metricInner y + (covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) + (manifoldGradient (I := I) g f y)) x v + = g.metricInner x + (covDerivAt g (fun y : M => - covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) x + covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) x (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f x) - + metricInner x - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x (v : TangentSpace I x)) - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x (v : TangentSpace I x)) + (manifoldGradient (I := I) g f x) + + g.metricInner x + (covDerivAt g (manifoldGradient (I := I) g f) x (v : TangentSpace I x)) + (covDerivAt g (manifoldGradient (I := I) g f) x (v : TangentSpace I x)) at h_compat2 rw [h_compat2] at h_bridge - -- Normalize `(∇[const v] const v) x` notation to `covDerivAt HasMetric.metric (const v) x v` (def-eq) + -- Normalize `(∇[const v] const v) x` notation to `covDerivAt g (const v) x v` (def-eq) -- to match the `secondCovDerivAt_def` unfolding. - change hessian (I := I) (M := M) HasMetric.metric (‖grad_g[I] f‖²_g) + change hessian (I := I) (M := M) g ((fun y => g.metricInner y (manifoldGradient (I := I) g f y) (manifoldGradient (I := I) g f y))) (fun _ : M => (v : TangentSpace I x)) (fun _ : M => (v : TangentSpace I x)) x = - 2 * (metricInner x - (covDerivAt HasMetric.metric + 2 * (g.metricInner x + (covDerivAt g (fun y : M => - covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) + covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) x (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f x) - + metricInner x - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x (v : TangentSpace I x)) - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x (v : TangentSpace I x))) - - 2 * metricInner x - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x - (covDerivAt HasMetric.metric (fun _ : M => (v : TangentSpace I x)) x + (manifoldGradient (I := I) g f x) + + g.metricInner x + (covDerivAt g (manifoldGradient (I := I) g f) x (v : TangentSpace I x)) + (covDerivAt g (manifoldGradient (I := I) g f) x (v : TangentSpace I x))) + - 2 * g.metricInner x + (covDerivAt g (manifoldGradient (I := I) g f) x + (covDerivAt g (fun _ : M => (v : TangentSpace I x)) x (v : TangentSpace I x))) - (manifoldGradient (I := I) HasMetric.metric f x) at h_bridge + (manifoldGradient (I := I) g f x) at h_bridge rw [h_bridge] have h_secondCD : - metricInner x - (secondCovDerivAt (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x v v) - (manifoldGradient (I := I) HasMetric.metric f x) - = metricInner x - (covDerivAt HasMetric.metric + g.metricInner x + (secondCovDerivAt (I := I) (M := M) g (manifoldGradient (I := I) g f) x v v) + (manifoldGradient (I := I) g f x) + = g.metricInner x + (covDerivAt g (fun y : M => - covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y (v : TangentSpace I x)) + covDerivAt g (manifoldGradient (I := I) g f) y (v : TangentSpace I x)) x (v : TangentSpace I x)) - (manifoldGradient (I := I) HasMetric.metric f x) - - metricInner x - (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x - (covDerivAt HasMetric.metric (fun _ : M => (v : TangentSpace I x)) x + (manifoldGradient (I := I) g f x) + - g.metricInner x + (covDerivAt g (manifoldGradient (I := I) g f) x + (covDerivAt g (fun _ : M => (v : TangentSpace I x)) x (v : TangentSpace I x))) - (manifoldGradient (I := I) HasMetric.metric f x) := by - rw [secondCovDerivAt_def, metricInner_sub_left] + (manifoldGradient (I := I) g f x) := by + rw [secondCovDerivAt_def, g.metricInner_sub_left] linarith [h_secondCD] diff --git a/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean b/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean index a1f9b12..d00c796 100644 --- a/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean +++ b/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean @@ -579,5 +579,19 @@ theorem bochner_connectionLaplacian_grad_decomposition -- composing this file's `bochner_connectionLaplacian_grad_decomposition` -- with the anchor's `bochner_leibniz_trace_reduction`. +/-- **Math.** **Explicit-`g` form of the heart-of-Bochner reduction**. -/ +theorem bochner_connectionLaplacian_grad_decomposition_g + [IsManifold I 2 M] [T2Space M] + (g : RiemannianMetric I M) (hg : g = hm.metric) + (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) : + g.metricInner x (connectionLaplacian g (manifoldGradient (I := I) g f) x) + (manifoldGradient (I := I) g f x) + = g.metricInner x (manifoldGradient (I := I) g f x) + (manifoldGradient (I := I) g (Operators.scalarLaplacian g f) x) + + ricciTensor g x (manifoldGradient (I := I) g f x) + (manifoldGradient (I := I) g f x) := by + subst hg + exact bochner_connectionLaplacian_grad_decomposition f hf x + end Operators end Riemannian diff --git a/OpenGALib/Riemannian/Util/MetricInnerSmoothness.lean b/OpenGALib/Riemannian/Util/MetricInnerSmoothness.lean index f7587ce..b255444 100644 --- a/OpenGALib/Riemannian/Util/MetricInnerSmoothness.lean +++ b/OpenGALib/Riemannian/Util/MetricInnerSmoothness.lean @@ -116,6 +116,17 @@ theorem metricInner_mdifferentiable (fun y => g.metricInner y (v y) (w y)) := fun y => g.metricInner_mdifferentiableAt (hv y) (hw y) +/-- **Eng.** `TangentSmoothAt`-form pointwise differentiability — convenience +wrapper that converts the framework's `TangentSmoothAt` predicate to +the underlying `MDifferentiableAt` bundle-section form. Explicit-`g` variant. -/ +theorem metricInner_mdifferentiableAt_of_tangentSmoothAt + (g : RiemannianMetric I M) + {Y Z : ∀ y : M, TangentSpace I y} + (hY : TangentSmoothAt Y x) (hZ : TangentSmoothAt Z x) : + MDifferentiableAt I 𝓘(ℝ, ℝ) + (fun y => g.metricInner y (Y y) (Z y)) x := + g.metricInner_mdifferentiableAt hY.toBundleSection hZ.toBundleSection + end Smoothness end Riemannian.RiemannianMetric