Gradient

DefinitionThe dot product with a fixed vector#✓fully proved

For a finite type \(\iota\) and a vector \(x \in \mathbb{R}^\iota\), this is the map \(v \mapsto v \cdot x = \sum_{i \in \iota} v_i x_i\), as a continuous linear functional \(\mathbb{R}^\iota \to \mathbb{R}\).

noncomputable def dotL (x : ι → ℝ) : (ι → ℝ) →L[ℝ] ℝ :=
  ∑ i, x i • ContinuousLinearMap.proj i

Used by 2

Used byDirectional derivative from the gradient · A Fréchet derivative given by a dot product is a gradient

TheoremA Fréchet derivative given by a dot product is a gradient#✓fully proved

Let \(\iota\) be a finite type, let \(f : \mathbb{R}^\iota \to \mathbb{R}\) and \(g, z \in \mathbb{R}^\iota\), and suppose that, for the sup norm on \(\mathbb{R}^\iota\), \(f\) is Fréchet differentiable at \(z\) with derivative \(v \mapsto v \cdot g\). Then \(f\), viewed as a function on the Euclidean space \(\mathbb{R}^\iota\) with inner product \(\langle v, w \rangle = \sum_{i \in \iota} v_i w_i\), has gradient \(g\) at \(z\).

theorem hasGradientAt_ofLp {f : (ι → ℝ) → ℝ} {g z : ι → ℝ} (hf : HasFDerivAt f (dotL g) z) :
    HasGradientAt (fun w : EuclideanSpace ℝ ι => f (WithLp.ofLp w)) (WithLp.toLp 2 g)
      (WithLp.toLp 2 z)

Uses 1

Statement usesThe dot product with a fixed vector

TheoremDirectional derivative from the gradient#✓fully proved

Let \(\iota\) be a finite type, let \(f : \mathbb{R}^\iota \to \mathbb{R}\) and \(g, z \in \mathbb{R}^\iota\), and suppose \(f\) is Fréchet differentiable at \(z\) with derivative \(w \mapsto w \cdot g\). Then for every \(v \in \mathbb{R}^\iota\), the function \(t \mapsto f(z + t v)\) on \(\mathbb{R}\) has derivative \(v \cdot g\) at \(t = 0\).

theorem hasDerivAt_line_of_hasFDerivAt {f : (ι → ℝ) → ℝ} {g z : ι → ℝ}
    (hf : HasFDerivAt f (dotL g) z) (v : ι → ℝ) :
    HasDerivAt (fun t : ℝ => f (z + t • v)) (v ⬝ᵥ g) 0

Uses 1

Statement usesThe dot product with a fixed vector

TheoremThe chain rule for gradients#✓fully proved

Let \(E\) and \(F\) be real Hilbert spaces, let \(g : E \to F\) be differentiable at \(x \in E\), and let \(f : F \to \mathbb{R}\) be differentiable at \(g(x)\). Then \(\nabla (f \circ g)(x) = Dg(x)^* \, \nabla f(g(x))\), where \(Dg(x) : E \to F\) is the Fréchet derivative of \(g\) at \(x\) and \(Dg(x)^*\) is its adjoint.

theorem gradient_comp {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F]
    {f : F → ℝ} {g : E → F} {x : E} (hf : DifferentiableAt ℝ f (g x))
    (hg : DifferentiableAt ℝ g x) :
    ∇ (f ∘ g) x = adjoint (fderiv ℝ g x) (∇ f (g x))

Used by 2

Used byBackpropagation computes the input gradient · Backpropagation computes the parameter gradients

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.