Theorems · Theorem · differential geometry

CovariantDerivative.derivMetricTensor_apply_eq_extend

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] {V : M → Type u_5}
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → NormedAddCommGroup (V x)]
  [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] [inst_10 : FiberBundle F V] (cov : CovariantDerivative I F V)
  [inst_11 : VectorBundle ℝ F V] [inst_12 : IsContMDiffRiemannianBundle I 1 F V] {x : M}
  [inst_13 : ContMDiffVectorBundle 1 F V I] [inst_14 : FiniteDimensional ℝ F] (X₀ : TangentSpace I x) (σ₀ τ₀ : V x),
  (((cov.derivMetricTensor x) σ₀) τ₀) X₀ =
    ((d% fun x_1 => inner ℝ (FiberBundle.extend F σ₀ x_1) (FiberBundle.extend F τ₀ x_1)) x) X₀ -
        inner ℝ ((↑cov (FiberBundle.extend F σ₀) x) X₀) τ₀ -
      inner ℝ σ₀ ((↑cov (FiberBundle.extend F τ₀) x) X₀)

Defined in

Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Cited by

0 results in Mathlib

Foundations

Depth 230 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupInnerProductSpaceFiberBundleVectorBundleIsContMDiffRiemannianBundleContMDiffVectorBundleFiniteDimensional