Derivatives of the norm

DefinitionReal part of the inner product as a real-linear functional#✓fully proved

The real-linear functional y ↦ re ⟪x, y⟫, the unnormalized gradient of the norm at x. The scalar field K is an explicit argument because the type E →L[ℝ] ℝ does not determine it.

noncomputable def reInnerSL (K : Type*) [RCLike K] {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace K E] [NormedSpace ℝ E] (x : E) : E →L[ℝ] ℝ :=
  (RCLike.reCLM (K := K)).comp ((innerSL K x).restrictScalars ℝ)

Used by 16

Used byDerivative of the squared distance to a point applied to a vector · Formula for the derivative of the norm · Derivative of the norm applied to a vector · Fréchet derivative of the norm at a nonzero point · Strict derivative of the squared distance to a point · Strict derivative of the squared distance to a subspace · Strict Fréchet derivative of the norm at a nonzero point · Strict derivative of the norm in a real inner product space · Strict derivative of the squared norm · Strict derivative of the squared projection residual · Chain rule for the strict derivative of a norm · Chain rule for the Fréchet derivative of a norm · Derivative of the norm along a curve · Derivative of the norm has operator norm one · Operator norm of the real inner product functional · Over the reals the norming functional is the inner product

TheoremStrict derivative of the squared norm#✓fully proved

The derivative of the squared norm is twice the real inner product with x.

theorem hasStrictFDerivAt_norm_sq (x : E) : HasStrictFDerivAt (fun y : E => ‖y‖ ^ 2)
    (2 • reInnerSL K x) x

Uses 1 · Used by 3

Statement usesReal part of the inner product as a real-linear functional

Used byStrict derivative of the squared distance to a point · Strict Fréchet derivative of the norm at a nonzero point · Strict derivative of the squared projection residual

TheoremStrict Fréchet derivative of the norm at a nonzero point#✓fully proved

The Fréchet derivative of the norm at a nonzero point x is the norming functional y ↦ re ⟪x, y⟫ / ‖x‖.

theorem hasStrictFDerivAt_norm {x : E} (hx : x ≠ 0) :
    HasStrictFDerivAt (fun y : E => ‖y‖) ((‖x‖⁻¹ : ℝ) • reInnerSL K x) x

Uses 2 · Used by 3

Statement usesReal part of the inner product as a real-linear functional

Proof usesStrict derivative of the squared norm

Used byFréchet derivative of the norm at a nonzero point · Strict derivative of the norm in a real inner product space · Chain rule for the strict derivative of a norm

TheoremFréchet derivative of the norm at a nonzero point#✓fully proved

The non-strict form of hasStrictFDerivAt_norm.

theorem hasFDerivAt_norm {x : E} (hx : x ≠ 0) :
    HasFDerivAt (fun y : E => ‖y‖) ((‖x‖⁻¹ : ℝ) • reInnerSL K x) x

Uses 2 · Used by 2

Statement usesReal part of the inner product as a real-linear functional

Proof usesStrict Fréchet derivative of the norm at a nonzero point

Used byFormula for the derivative of the norm · Chain rule for the Fréchet derivative of a norm

TheoremFormula for the derivative of the norm#✓fully proved

The fderiv of the norm at a nonzero point.

theorem fderiv_norm {x : E} (hx : x ≠ 0) :
    fderiv ℝ (fun y : E => ‖y‖) x = (‖x‖⁻¹ : ℝ) • reInnerSL K x

Uses 2 · Used by 2

Statement usesReal part of the inner product as a real-linear functional

Proof usesFréchet derivative of the norm at a nonzero point

Used byDerivative of the norm applied to a vector · Derivative of the norm has operator norm one

TheoremDerivative of the norm applied to a vector#✓fully proved

The fderiv of the norm at a nonzero point, applied to a vector.

theorem fderiv_norm_apply {x y : E} (hx : x ≠ 0) :
    fderiv ℝ (fun z : E => ‖z‖) x y = RCLike.re (inner K x y) / ‖x‖

Uses 2 · Used by 1

Proof usesFormula for the derivative of the norm · Real part of the inner product as a real-linear functional

Used byDerivative of the norm in a real space applied to a vector

TheoremOperator norm of the real inner product functional#✓fully proved

The norming functional reInnerSL K x has operator norm ‖x‖ (it attains ‖x‖ at ‖x‖⁻¹ • x).

theorem norm_reInnerSL (x : E) : ‖reInnerSL K x‖ = ‖x‖

Uses 1 · Used by 1

Statement usesReal part of the inner product as a real-linear functional

Used byDerivative of the norm has operator norm one

TheoremDerivative of the norm has operator norm one#✓fully proved

The Fréchet derivative of the norm at a nonzero point has operator norm 1: the norming functional is a norming functional. This statement needs the inner product structure, so K is an explicit argument.

theorem norm_fderiv_norm (K : Type*) [RCLike K] [InnerProductSpace K E] {x : E}
    (hx : x ≠ 0) :
    ‖fderiv ℝ (fun y : E => ‖y‖) x‖ = 1

Uses 3

Proof usesFormula for the derivative of the norm · Operator norm of the real inner product functional · Real part of the inner product as a real-linear functional

TheoremOver the reals the norming functional is the inner product#✓fully proved

Over ℝ, the norming functional is just innerSL ℝ x.

theorem reInnerSL_real {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (x : E) : reInnerSL ℝ x = innerSL ℝ x

Uses 1 · Used by 1

Statement usesReal part of the inner product as a real-linear functional

Used byStrict derivative of the norm in a real inner product space

TheoremStrict derivative of the norm in a real inner product space#✓fully proved

The Fréchet derivative of the norm in a real inner product space.

theorem hasStrictFDerivAt_norm_real {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] {x : E} (hx : x ≠ 0) :
    HasStrictFDerivAt (fun y : E => ‖y‖) ((‖x‖⁻¹ : ℝ) • innerSL ℝ x) x

Uses 3

Proof usesStrict Fréchet derivative of the norm at a nonzero point · Real part of the inner product as a real-linear functional · Over the reals the norming functional is the inner product

TheoremDerivative of the norm in a real space applied to a vector#✓fully proved

The fderiv of the norm in a real inner product space, applied to a vector.

theorem fderiv_norm_apply_real {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    {x y : E} (hx : x ≠ 0) :
    fderiv ℝ (fun z : E => ‖z‖) x y = inner ℝ x y / ‖x‖

Uses 1

Proof usesDerivative of the norm applied to a vector

TheoremChain rule for the strict derivative of a norm#✓fully proved

Chain rule: the derivative of the norm of a differentiable map.

theorem HasStrictFDerivAt.norm {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
    {f : G → E} {f' : G →L[ℝ] E} {x : G} (hf : HasStrictFDerivAt f f' x)
    (h0 : f x ≠ 0) :
    HasStrictFDerivAt (fun y => ‖f y‖)
      (((‖f x‖⁻¹ : ℝ) • reInnerSL K (f x)).comp f') x

Uses 2

Statement usesReal part of the inner product as a real-linear functional

Proof usesStrict Fréchet derivative of the norm at a nonzero point

TheoremChain rule for the Fréchet derivative of a norm#✓fully proved

Chain rule: the non-strict derivative of the norm of a differentiable map.

theorem HasFDerivAt.norm {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
    {f : G → E} {f' : G →L[ℝ] E} {x : G} (hf : HasFDerivAt f f' x)
    (h0 : f x ≠ 0) :
    HasFDerivAt (fun y => ‖f y‖)
      (((‖f x‖⁻¹ : ℝ) • reInnerSL K (f x)).comp f') x

Uses 2 · Used by 1

Statement usesReal part of the inner product as a real-linear functional

Proof usesFréchet derivative of the norm at a nonzero point

Used byDerivative of the norm along a curve

TheoremDerivative of the norm along a curve#✓fully proved

The derivative of the norm along a curve is the normalized real inner product of the position with the velocity.

theorem HasDerivAt.norm {f : ℝ → E} {f' : E} {t : ℝ} (hf : HasDerivAt f f' t)
    (h0 : f t ≠ 0) :
    HasDerivAt (fun t => ‖f t‖) (RCLike.re (inner K (f t) f') / ‖f t‖) t

Uses 2 · Used by 1

Proof usesChain rule for the Fréchet derivative of a norm · Real part of the inner product as a real-linear functional

Used byCurves on the unit sphere have velocity orthogonal to position

TheoremCurves on the unit sphere have velocity orthogonal to position#✓fully proved

A differentiable curve lying on the unit sphere has velocity orthogonal to its position (in the real-inner-product sense).

theorem re_inner_self_deriv_eq_zero_of_forall_norm_eq_one {γ : ℝ → E}
    (hγ : Differentiable ℝ γ) (h1 : ∀ t, ‖γ t‖ = 1) (t : ℝ) :
    RCLike.re (inner K (γ t) (deriv γ t)) = 0

Uses 1

Proof usesDerivative of the norm along a curve

TheoremStrict derivative of the squared distance to a point#✓fully proved

The gradient of the squared distance to a point a is 2 • reInnerSL K (x - a).

theorem hasStrictFDerivAt_dist_sq {x a : E} :
    HasStrictFDerivAt (fun y : E => dist y a ^ 2) (2 • reInnerSL K (x - a)) x

Uses 2 · Used by 1

Statement usesReal part of the inner product as a real-linear functional

Proof usesStrict derivative of the squared norm

Used byDerivative of the squared distance to a point applied to a vector

TheoremDerivative of the squared distance to a point applied to a vector#✓fully proved

The fderiv of the squared distance to a point, applied to a vector.

theorem fderiv_dist_sq_apply {x a y : E} :
    fderiv ℝ (fun z : E => dist z a ^ 2) x y = 2 * RCLike.re (inner K (x - a) y)

Uses 2

Proof usesStrict derivative of the squared distance to a point · Real part of the inner product as a real-linear functional

TheoremDistance to a subspace as the norm of the projection residual#✓fully proved

The distance from y to a subspace with an orthogonal projection is the norm of the residual y - S.starProjection y.

theorem infDist_eq_norm_sub_starProjection {S : Submodule K E} [S.HasOrthogonalProjection]
    (y : E) :
    Metric.infDist y (S : Set E) = ‖y - S.starProjection y‖

Used by 1

Used byStrict derivative of the squared distance to a subspace

TheoremStrict derivative of the squared projection residual#✓fully proved

The gradient of the squared residual ‖y - S.starProjection y‖ ^ 2 is 2 • reInnerSL K (x - S.starProjection x), using that the residual operator 1 - S.starProjection is self-adjoint and idempotent.

theorem hasStrictFDerivAt_residual_sq {S : Submodule K E} [S.HasOrthogonalProjection]
    (x : E) :
    HasStrictFDerivAt (fun y : E => ‖y - S.starProjection y‖ ^ 2)
      (2 • reInnerSL K (x - S.starProjection x)) x

Uses 2 · Used by 1

Statement usesReal part of the inner product as a real-linear functional

Proof usesStrict derivative of the squared norm

Used byStrict derivative of the squared distance to a subspace

TheoremStrict derivative of the squared distance to a subspace#✓fully proved

The gradient of the squared distance to a subspace S is twice the real inner product with the residual x - S.starProjection x.

theorem hasStrictFDerivAt_infDist_sq {S : Submodule K E} [S.HasOrthogonalProjection]
    (x : E) :
    HasStrictFDerivAt (fun y : E => Metric.infDist y (S : Set E) ^ 2)
      (2 • reInnerSL K (x - S.starProjection x)) x

Uses 3

Statement usesReal part of the inner product as a real-linear functional

Proof usesStrict derivative of the squared projection residual · Distance to a subspace as the norm of the projection residual

TheoremSecond derivative of the squared norm#✓fully proved

Let \(E\) be a real inner product space. For all \(p, u, v \in E\), the second Fréchet derivative of \(x \mapsto \|x\|^2\) at \(p\), applied to \(u\) and then to \(v\), equals \(2 \langle u, v \rangle\).

theorem fderiv_fderiv_norm_sq_apply (p u v : E) :
    fderiv ℝ (fderiv ℝ (fun x : E ↦ ‖x‖ ^ 2)) p u v = 2 * inner ℝ u v

Used by 6

Used byMean curvature of the unit sphere · Euclidean Finsler metric · Laplacian of the Gaussian potential · Laplacian of the squared norm · The Gaussian gradient Ricci soliton · Gaussian potentials that are gradient Ricci solitons

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.