# Documentation

## Main Definitions #

Let f be a function from a Hilbert Space F to 𝕜 (𝕜 is ℝ or ℂ) , x be a point in F and f' be a vector in F. Then

HasGradientWithinAt f f' s x

says that f has a gradient f' at x, where the domain of interest is restricted to s. We also have

HasGradientAt f f' x := HasGradientWithinAt f f' x univ

## Main results #

This file contains the following parts of gradient.

• the theorems translating between HasGradientAtFilter and HasFDerivAtFilter, HasGradientWithinAt and HasFDerivWithinAt, HasGradientAt and HasFDerivAt, Gradient and fderiv.
• theorems the Uniqueness of Gradient.
• the theorems translating between HasGradientAtFilter and HasDerivAtFilter, HasGradientAt and HasDerivAt, Gradient and deriv when F = 𝕜.
def HasGradientAtFilter {𝕜 : Type u_1} {F : Type u_2} [] [] [] (f : F𝕜) (f' : F) (x : F) (L : ) :

A function f has the gradient f' as derivative along the filter L if f x' = f x + ⟨f', x' - x⟩ + o (x' - x) when x' converges along the filter L.

Equations
Instances For
def HasGradientWithinAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] (f : F𝕜) (f' : F) (s : Set F) (x : F) :

f has the gradient f' at the point x within the subset s if f x' = f x + ⟨f', x' - x⟩ + o (x' - x) where x' converges to x inside s.

Equations
Instances For
def HasGradientAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] (f : F𝕜) (f' : F) (x : F) :

f has the gradient f' at the point x if f x' = f x + ⟨f', x' - x⟩ + o (x' - x) where x' converges to x.

Equations
Instances For
def gradientWithin {𝕜 : Type u_1} {F : Type u_2} [] [] [] (f : F𝕜) (s : Set F) (x : F) :
F

Gradient of f at the point x within the set s, if it exists. Zero otherwise.

If the derivative exists (i.e., ∃ f', HasGradientWithinAt f f' s x), then f x' = f x + ⟨f', x' - x⟩ + o (x' - x) where x' converges to x inside s.

Equations
Instances For
def gradient {𝕜 : Type u_1} {F : Type u_2} [] [] [] (f : F𝕜) (x : F) :
F

Gradient of f at the point x, if it exists. Zero otherwise.

If the derivative exists (i.e., ∃ f', HasGradientAt f f' x), then f x' = f x + ⟨f', x' - x⟩ + o (x' - x) where x' converges to x.

Equations
Instances For

Gradient of f at the point x, if it exists. Zero otherwise.

If the derivative exists (i.e., ∃ f', HasGradientAt f f' x), then f x' = f x + ⟨f', x' - x⟩ + o (x' - x) where x' converges to x.

Equations
Instances For
theorem hasGradientWithinAt_iff_hasFDerivWithinAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {s : Set F} :
theorem hasFDerivWithinAt_iff_hasGradientWithinAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {x : F} {frechet : F →L[𝕜] 𝕜} {s : Set F} :
HasFDerivWithinAt f frechet s x HasGradientWithinAt f ( frechet) s x
theorem hasGradientAt_iff_hasFDerivAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} :
HasGradientAt f f' x HasFDerivAt f (() f') x
theorem hasFDerivAt_iff_hasGradientAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {x : F} {frechet : F →L[𝕜] 𝕜} :
HasFDerivAt f frechet x HasGradientAt f ( frechet) x
theorem HasGradientWithinAt.hasFDerivWithinAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {s : Set F} :
HasGradientWithinAt f f' s xHasFDerivWithinAt f (() f') s x

Alias of the forward direction of hasGradientWithinAt_iff_hasFDerivWithinAt.

theorem HasFDerivWithinAt.hasGradientWithinAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {x : F} {frechet : F →L[𝕜] 𝕜} {s : Set F} :
HasFDerivWithinAt f frechet s xHasGradientWithinAt f ( frechet) s x

Alias of the forward direction of hasFDerivWithinAt_iff_hasGradientWithinAt.

theorem HasGradientAt.hasFDerivAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} :
HasGradientAt f f' xHasFDerivAt f (() f') x

Alias of the forward direction of hasGradientAt_iff_hasFDerivAt.

theorem HasFDerivAt.hasGradientAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {x : F} {frechet : F →L[𝕜] 𝕜} :
HasFDerivAt f frechet xHasGradientAt f ( frechet) x

Alias of the forward direction of hasFDerivAt_iff_hasGradientAt.

theorem gradient_eq_zero_of_not_differentiableAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {x : F} (h : ¬) :
theorem DifferentiableAt.hasGradientAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {x : F} (h : ) :
theorem HasGradientAt.differentiableAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} (h : HasGradientAt f f' x) :
theorem DifferentiableWithinAt.hasGradientWithinAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {x : F} {s : Set F} (h : ) :
theorem HasGradientWithinAt.differentiableWithinAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {s : Set F} (h : HasGradientWithinAt f f' s x) :
@[simp]
theorem hasGradientWithinAt_univ {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} :
theorem DifferentiableOn.hasGradientAt {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {x : F} {s : Set F} (h : ) (hs : s nhds x) :
theorem HasGradientAt.gradient {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} (h : HasGradientAt f f' x) :
theorem gradient_eq {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : FF} (h : ∀ (x : F), HasGradientAt f (f' x) x) :
= f'
theorem HasGradientAtFilter.hasDerivAtFilter {𝕜 : Type u_1} [] {g : 𝕜𝕜} {g' : 𝕜} {u : 𝕜} {L' : } (h : HasGradientAtFilter g g' u L') :
HasDerivAtFilter g (() g') u L'
theorem HasDerivAtFilter.hasGradientAtFilter {𝕜 : Type u_1} [] {g : 𝕜𝕜} {g' : 𝕜} {u : 𝕜} {L' : } (h : HasDerivAtFilter g g' u L') :
HasGradientAtFilter g (() g') u L'
theorem HasGradientAt.hasDerivAt {𝕜 : Type u_1} [] {g : 𝕜𝕜} {g' : 𝕜} {u : 𝕜} (h : HasGradientAt g g' u) :
HasDerivAt g (() g') u
theorem HasDerivAt.hasGradientAt {𝕜 : Type u_1} [] {g : 𝕜𝕜} {g' : 𝕜} {u : 𝕜} (h : HasDerivAt g g' u) :
theorem gradient_eq_deriv {𝕜 : Type u_1} [] {g : 𝕜𝕜} {u : 𝕜} :
gradient g u = () (deriv g u)
theorem HasGradientAtFilter.hasDerivAtFilter' {g : } {g' : } {u : } {L' : } (h : HasGradientAtFilter g g' u L') :
theorem HasDerivAtFilter.hasGradientAtFilter' {g : } {g' : } {u : } {L' : } (h : HasDerivAtFilter g g' u L') :
theorem HasGradientAt.hasDerivAt' {g : } {g' : } {u : } (h : HasGradientAt g g' u) :
HasDerivAt g g' u
theorem HasDerivAt.hasGradientAt' {g : } {g' : } {u : } (h : HasDerivAt g g' u) :
theorem gradient_eq_deriv' {g : } {u : } :
gradient g u = deriv g u
theorem hasGradientAtFilter_iff_isLittleO {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {L : } :
HasGradientAtFilter f f' x L (fun (x' : F) => f x' - f x - inner f' (x' - x)) =o[L] fun (x' : F) => x' - x
theorem hasGradientWithinAt_iff_isLittleO {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {s : Set F} :
HasGradientWithinAt f f' s x (fun (x' : F) => f x' - f x - inner f' (x' - x)) =o[] fun (x' : F) => x' - x
theorem hasGradientWithinAt_iff_tendsto {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {s : Set F} :
HasGradientWithinAt f f' s x Filter.Tendsto (fun (x' : F) => x' - x⁻¹ * f x' - f x - inner f' (x' - x)) () (nhds 0)
theorem hasGradientAt_iff_isLittleO {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} :
HasGradientAt f f' x (fun (x' : F) => f x' - f x - inner f' (x' - x)) =o[nhds x] fun (x' : F) => x' - x
theorem hasGradientAt_iff_tendsto {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} :
HasGradientAt f f' x Filter.Tendsto (fun (x' : F) => x' - x⁻¹ * f x' - f x - inner f' (x' - x)) (nhds x) (nhds 0)
theorem HasGradientAtFilter.isBigO_sub {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {L : } (h : HasGradientAtFilter f f' x L) :
(fun (x' : F) => f x' - f x) =O[L] fun (x' : F) => x' - x
theorem hasGradientWithinAt_congr_set' {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {s : Set F} {t : Set F} (y : F) (h : s =ᶠ[nhdsWithin x {y}] t) :
theorem hasGradientWithinAt_congr_set {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {s : Set F} {t : Set F} (h : s =ᶠ[nhds x] t) :
theorem hasGradientAt_iff_isLittleO_nhds_zero {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} :
HasGradientAt f f' x (fun (h : F) => f (x + h) - f x - inner f' h) =o[nhds 0] fun (h : F) => h

### Congruence properties of the Gradient #

theorem Filter.EventuallyEq.hasGradientAtFilter_iff {𝕜 : Type u_1} {F : Type u_2} [] [] [] {x : F} {L : } {f₀ : F𝕜} {f₁ : F𝕜} {f₀' : F} {f₁' : F} (h₀ : f₀ =ᶠ[L] f₁) (hx : f₀ x = f₁ x) (h₁ : f₀' = f₁') :
theorem HasGradientAtFilter.congr_of_eventuallyEq {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {L : } {f₁ : F𝕜} (h : HasGradientAtFilter f f' x L) (hL : f₁ =ᶠ[L] f) (hx : f₁ x = f x) :
theorem HasGradientWithinAt.congr_mono {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {s : Set F} {f₁ : F𝕜} {t : Set F} (h : HasGradientWithinAt f f' s x) (ht : xt, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t s) :
theorem HasGradientWithinAt.congr {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {s : Set F} {f₁ : F𝕜} (h : HasGradientWithinAt f f' s x) (hs : xs, f₁ x = f x) (hx : f₁ x = f x) :
theorem HasGradientWithinAt.congr_of_mem {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {s : Set F} {f₁ : F𝕜} (h : HasGradientWithinAt f f' s x) (hs : xs, f₁ x = f x) (hx : x s) :
theorem HasGradientWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {s : Set F} {f₁ : F𝕜} (h : HasGradientWithinAt f f' s x) (h₁ : f₁ =ᶠ[] f) (hx : f₁ x = f x) :
theorem HasGradientWithinAt.congr_of_eventuallyEq_of_mem {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {s : Set F} {f₁ : F𝕜} (h : HasGradientWithinAt f f' s x) (h₁ : f₁ =ᶠ[] f) (hx : x s) :
theorem HasGradientAt.congr_of_eventuallyEq {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {f' : F} {x : F} {f₁ : F𝕜} (h : HasGradientAt f f' x) (h₁ : f₁ =ᶠ[nhds x] f) :
theorem Filter.EventuallyEq.gradient_eq {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {x : F} {f₁ : F𝕜} (hL : f₁ =ᶠ[nhds x] f) :
theorem Filter.EventuallyEq.gradient {𝕜 : Type u_1} {F : Type u_2} [] [] [] {f : F𝕜} {x : F} {f₁ : F𝕜} (h : f₁ =ᶠ[nhds x] f) :

### The Gradient of constant functions #

theorem hasGradientAtFilter_const {𝕜 : Type u_1} {F : Type u_2} [] [] [] (x : F) (L : ) (c : 𝕜) :
HasGradientAtFilter (fun (x : F) => c) 0 x L
theorem hasGradientWithinAt_const {𝕜 : Type u_1} {F : Type u_2} [] [] [] (x : F) (s : Set F) (c : 𝕜) :
HasGradientWithinAt (fun (x : F) => c) 0 s x
theorem hasGradientAt_const {𝕜 : Type u_1} {F : Type u_2} [] [] [] (x : F) (c : 𝕜) :
HasGradientAt (fun (x : F) => c) 0 x
theorem gradient_const {𝕜 : Type u_1} {F : Type u_2} [] [] [] (x : F) (c : 𝕜) :
gradient (fun (x : F) => c) x = 0
@[simp]
theorem gradient_const' {𝕜 : Type u_1} [] (c : 𝕜) :
(gradient fun (x : 𝕜) => c) = fun (x : 𝕜) => 0