The gradient on a normed space

On a flat inner product space with its standard Riemannian metric, the manifold gradient agrees with Mathlib's gradient; the squared norm therefore has the expected radial gradient. For an arbitrary Riemannian metric on a normed space, the gradient is read in linear coordinates through its pairing with constant vectors, and its squared length is |dφ|² = dφ(g⁻¹ dφ) for the metric coefficient field g.

The standard metric is analytic (IsContMDiffRiemannianBundle.vectorSpace), so the manifold results on gradient flows apply to it, and a classical solution of γ' = -∇ f (γ) on an open interval around 0 is the maximal integral curve of -grad f there (TauCeti.Manifold.eqOn_maximalIntegralCurve_neg_mgradient_of_hasDerivAt).

theorem TauCeti.Manifold.inner_tangentSpace_vectorSpace {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} (v w : TangentSpace (modelWithCornersSelf ℝ F) x) : inner ℝ v w = inner ℝ ((NormedSpace.fromTangentSpace x) v) ((NormedSpace.fromTangentSpace x) w)

The canonical identification of a tangent space of a real inner-product space with the model space preserves inner products.

theorem TauCeti.Manifold.mgradient_eq_gradient {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (f : F → ℝ) (x : F) : have x_1 := { g := (riemannianMetricVectorSpace F).toRiemannianMetric }; mgradient (modelWithCornersSelf ℝ F) f x = gradient f x

On a flat inner product space with its standard Riemannian metric, the manifold gradient is Mathlib's gradient.

theorem TauCeti.Manifold.mgradient_eq_gradient_of_eq {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [inst : Bundle.RiemannianBundle fun (x : F) => TangentSpace (modelWithCornersSelf ℝ F) x] (hg : Bundle.RiemannianBundle.g = (riemannianMetricVectorSpace F).toRiemannianMetric) (f : F → ℝ) (x : F) : mgradient (modelWithCornersSelf ℝ F) f x = gradient f x

If the installed fibre metric is the standard one, the manifold gradient is Mathlib's gradient. This transports mgradient_eq_gradient along an equality of fibre metrics, such as toRiemannianMetric_ofLE, which cannot be rewritten inside the instance-dependent arguments.

theorem TauCeti.Manifold.norm_mgradient_eq_norm_gradient_of_eq {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [inst : Bundle.RiemannianBundle fun (x : F) => TangentSpace (modelWithCornersSelf ℝ F) x] (hg : Bundle.RiemannianBundle.g = (riemannianMetricVectorSpace F).toRiemannianMetric) (f : F → ℝ) (x : F) : ‖mgradient (modelWithCornersSelf ℝ F) f x‖ = ‖gradient f x‖

If the installed fibre metric is the standard one, the manifold gradient has the norm of Mathlib's gradient. The norm on the tangent space is itself induced by the installed metric, so this is transported along hg together with mgradient_eq_gradient_of_eq.

@[simp]

theorem TauCeti.Manifold.mgradient_norm_sq_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (x : F) : have x_1 := { g := (riemannianMetricVectorSpace F).toRiemannianMetric }; mgradient (modelWithCornersSelf ℝ F) (fun (y : F) => ‖y‖ ^ 2) x = 2 • x

The gradient of the squared norm in the standard flat metric is the radial vector field.

Source: Mathlib.Analysis.InnerProductSpace.Calculus.fderiv_norm_sq_apply.

theorem TauCeti.Manifold.inner_mgradient_model_space {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [Bundle.RiemannianBundle fun (x : F) => TangentSpace (modelWithCornersSelf ℝ F) x] (f : F → ℝ) (x v : F) : inner ℝ (mgradient (modelWithCornersSelf ℝ F) f x) ((tangentSpaceCastModel (modelWithCornersSelf ℝ F) x).symm v) = (fderiv ℝ f x) v

On a normed space with any Riemannian metric, pairing the gradient with a constant vector v gives the Fréchet derivative in the direction v.

theorem TauCeti.Manifold.norm_mgradient_sq_model_space {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [Bundle.RiemannianBundle fun (x : F) => TangentSpace (modelWithCornersSelf ℝ F) x] {g : F → F →L[ℝ] F →L[ℝ] ℝ} {x : F} (hg : ∀ (v w : TangentSpace (modelWithCornersSelf ℝ F) x), inner ℝ v w = ((g x) ((tangentSpaceCastModel (modelWithCornersSelf ℝ F) x) v)) ((tangentSpaceCastModel (modelWithCornersSelf ℝ F) x) w)) (f : F → ℝ) : ‖mgradient (modelWithCornersSelf ℝ F) f x‖ ^ 2 = (fderiv ℝ f x) ((g x).inverse (fderiv ℝ f x))

On a normed space whose Riemannian metric at x is the bilinear form g x in linear coordinates, the squared length of the gradient is |df|² = df(g⁻¹ df).

theorem TauCeti.Manifold.eqOn_maximalIntegralCurve_neg_mgradient_of_hasDerivAt {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {f : F → ℝ} (hf : ContDiff ℝ 2 f) {γ : ℝ → F} {a b : ℝ} (h0 : 0 ∈ Set.Ioo a b) (hγ : ∀ t ∈ Set.Ioo a b, HasDerivAt γ (-gradient f (γ t)) t) : Set.EqOn (maximalIntegralCurve (-mgradient (modelWithCornersSelf ℝ F) f) (γ 0)) γ (Set.Ioo a b)

Negative gradient trajectories of a flat space. On a finite-dimensional real inner product space with its standard metric, let f be C² and let γ solve γ' = -∇ f (γ) on an open interval around 0. Then γ is the maximal integral curve of -grad f through γ 0 on that interval.