Chain rules for Riemannian gradients

The gradient within a subset is the fibrewise Riesz dual of mvfderivWithin. This gives a relative gradient calculus on manifolds with boundary or corners, with unique differentiability required by the chain rules rather than by the definition.

For a map between Riemannian manifolds, the gradient of a composite is obtained by pulling the metric dual of the target gradient back along the differential, then taking the Riesz dual in the source. Thus the metric adjoint of the differential transports the target gradient to the source gradient. Scalar postcomposition gives grad (g ∘ f) = g'(f) • grad f.

The construction uses Riemannian.Tensor.rieszDual; the chain rules use Mathlib's mvfderivWithin_comp and its unrestricted specialization. No regularity of the metric beyond its pointwise Riemannian bundle structure is needed.

References

• John M. Lee, Introduction to Smooth Manifolds, second edition, Chapter 13.

theorem TauCeti.Manifold.inner_mgradientWithin_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {s : Set M} {x : M} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' 1 N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace I' y] {φ : M → N} {g : N → ℝ} {t : Set N} (hg : MDiffAt[t] g (φ x)) (hφ : MDiffAt[s] φ x) (hφt : Set.MapsTo φ s t) (hs : UniqueMDiffAt[s] x) (v : TangentSpace I x) : inner ℝ (mgradientWithin I (g ∘ φ) s x) v = inner ℝ (mgradientWithin I' g t (φ x)) ((mfderiv[s] φ x) v)

The relative gradient chain rule in inner-product form.

theorem TauCeti.Manifold.mgradientWithin_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {s : Set M} {x : M} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' 1 N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace I' y] {φ : M → N} {g : N → ℝ} {t : Set N} (hg : MDiffAt[t] g (φ x)) (hφ : MDiffAt[s] φ x) (hφt : Set.MapsTo φ s t) (hs : UniqueMDiffAt[s] x) : mgradientWithin I (g ∘ φ) s x = (Riemannian.Tensor.rieszDual x) ((innerSL ℝ) (mgradientWithin I' g t (φ x)) ∘SL mfderiv[s] φ x)

The relative gradient of a composite is the source Riesz dual of the pullback of the metric dual of the target gradient. This is the metric-adjoint chain rule.

theorem TauCeti.Manifold.inner_mgradient_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {x : M} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' 1 N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace I' y] {φ : M → N} {g : N → ℝ} (hg : MDiffAt g (φ x)) (hφ : MDiffAt φ x) (v : TangentSpace I x) : inner ℝ (mgradient I (g ∘ φ) x) v = inner ℝ (mgradient I' g (φ x)) ((mfderiv% φ x) v)

The gradient chain rule in inner-product form on the whole manifold.

theorem TauCeti.Manifold.mgradient_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {x : M} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' 1 N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace I' y] {φ : M → N} {g : N → ℝ} (hg : MDiffAt g (φ x)) (hφ : MDiffAt φ x) : mgradient I (g ∘ φ) x = (Riemannian.Tensor.rieszDual x) ((innerSL ℝ) (mgradient I' g (φ x)) ∘SL mfderiv% φ x)

The metric-adjoint gradient chain rule on the whole manifold.

theorem TauCeti.Manifold.mgradientWithin_comp_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {f : M → ℝ} {s : Set M} {x : M} {g : ℝ → ℝ} {g' : ℝ} {t : Set ℝ} (hg : HasDerivWithinAt g g' t (f x)) (hf : MDiffAt[s] f x) (hst : Set.MapsTo f s t) (hs : UniqueMDiffAt[s] x) : mgradientWithin I (g ∘ f) s x = g' • mgradientWithin I f s x

Scalar postcomposition multiplies the relative gradient by the scalar derivative. The outer derivative may itself be taken within a subset of the real line.

theorem TauCeti.Manifold.mgradientWithin_comp_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {f : M → ℝ} {s : Set M} {x : M} {g : ℝ → ℝ} {g' : ℝ} (hg : HasDerivAt g g' (f x)) (hf : MDiffAt[s] f x) (hs : UniqueMDiffAt[s] x) : mgradientWithin I (g ∘ f) s x = g' • mgradientWithin I f s x

Scalar postcomposition multiplies the relative gradient by the ordinary scalar derivative.

theorem TauCeti.Manifold.mgradient_comp_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {f : M → ℝ} {x : M} {g : ℝ → ℝ} {g' : ℝ} (hg : HasDerivAt g g' (f x)) (hf : MDiffAt f x) : mgradient I (g ∘ f) x = g' • mgradient I f x

Scalar postcomposition multiplies the gradient by the scalar derivative.

theorem TauCeti.Manifold.mgradientWithin_comp_deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {f : M → ℝ} {s : Set M} {x : M} {g : ℝ → ℝ} (hg : DifferentiableAt ℝ g (f x)) (hf : MDiffAt[s] f x) (hs : UniqueMDiffAt[s] x) : mgradientWithin I (g ∘ f) s x = deriv g (f x) • mgradientWithin I f s x

The relative gradient chain rule for differentiable scalar postcomposition.

theorem TauCeti.Manifold.mgradient_comp_deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {f : M → ℝ} {x : M} {g : ℝ → ℝ} (hg : DifferentiableAt ℝ g (f x)) (hf : MDiffAt f x) : mgradient I (g ∘ f) x = deriv g (f x) • mgradient I f x

The gradient chain rule for differentiable scalar postcomposition.

theorem TauCeti.Manifold.mgradient_log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {f : M → ℝ} {x : M} (hf : MDiffAt f x) : mgradient I (fun (y : M) => Real.log (f y)) x = (f x)⁻¹ • mgradient I f x

The gradient of the logarithm of a function: grad (log f) = f⁻¹ • grad f. At a zero of f both sides vanish, since Real.log 0 = 0 and 0⁻¹ = 0.