Theorems · Theorem · differential geometry

CovariantDerivative.derivMetricTensor_apply

∀ {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] {σ τ : (x : M) → V x}
  (cov : CovariantDerivative I F V) [inst_11 : VectorBundle ℝ F V] [inst_12 : IsContMDiffRiemannianBundle I 1 F V]
  {X : (x : M) → TangentSpace I x} [inst_13 : ContMDiffVectorBundle 1 F V I] [inst_14 : FiniteDimensional ℝ F] (x : M),
  MDiffAt (T% σ) x →
    MDiffAt (T% τ) x →
      (((cov.derivMetricTensor x) (σ x)) (τ x)) (X x) =
        ((d% fun x => inner ℝ (σ x) (τ x)) x) (X x) - (fun x => inner ℝ ((fun x => (↑cov σ x) (X x)) x) (τ x)) x -
          (fun x => inner ℝ (σ x) ((fun x => (↑cov τ x) (X x)) x)) x

Defined in

Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupInnerProductSpaceFiberBundleVectorBundleIsContMDiffRiemannianBundleContMDiffVectorBundleFiniteDimensional