Gradient

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 definition 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 = 𝕜.
• the theorems about the congruence of the gradient.
• the theorems about the gradient of constant function.
• the theorems about the continuity of a function admitting a gradient.

def HasGradientAtFilter {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (f : F → 𝕜) (f' x : F) (L : Filter F) : Prop

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

• HasGradientAtFilter f f' x L = HasFDerivAtFilter f ((InnerProductSpace.toDual 𝕜 F) f') x L

def HasGradientWithinAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (f : F → 𝕜) (f' : F) (s : Set F) (x : F) : Prop

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

• HasGradientWithinAt f f' s x = HasGradientAtFilter f f' x (nhdsWithin x s)

def HasGradientAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (f : F → 𝕜) (f' x : F) : Prop

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

• HasGradientAt f f' x = HasGradientAtFilter f f' x (nhds x)

def gradientWithin {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (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

• gradientWithin f s x = (InnerProductSpace.toDual 𝕜 F).symm (fderivWithin 𝕜 f s x)

def gradient {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (f : F → 𝕜) (x : F) : F

Gradient of f at the point x, if it exists. Zero otherwise. Denoted as ∇ within the Gradient namespace.

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

• gradient f x = (InnerProductSpace.toDual 𝕜 F).symm (fderiv 𝕜 f x)

def Gradient.«term∇» : Lean.ParserDescr

Gradient of f at the point x, if it exists. Zero otherwise. Denoted as ∇ within the Gradient namespace.

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

• Gradient.«term∇» = Lean.ParserDescr.node `Gradient.«term∇» 1024 (Lean.ParserDescr.symbol "∇")

theorem hasGradientWithinAt_iff_hasFDerivWithinAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} : HasGradientWithinAt f f' s x ↔ HasFDerivWithinAt f ((InnerProductSpace.toDual 𝕜 F) f') s x

theorem hasFDerivWithinAt_iff_hasGradientWithinAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} {frechet : F →L[𝕜] 𝕜} {s : Set F} : HasFDerivWithinAt f frechet s x ↔ HasGradientWithinAt f ((InnerProductSpace.toDual 𝕜 F).symm frechet) s x

theorem hasGradientAt_iff_hasFDerivAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} : HasGradientAt f f' x ↔ HasFDerivAt f ((InnerProductSpace.toDual 𝕜 F) f') x

theorem hasFDerivAt_iff_hasGradientAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} {frechet : F →L[𝕜] 𝕜} : HasFDerivAt f frechet x ↔ HasGradientAt f ((InnerProductSpace.toDual 𝕜 F).symm frechet) x

theorem HasGradientWithinAt.hasFDerivWithinAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} : HasGradientWithinAt f f' s x → HasFDerivWithinAt f ((InnerProductSpace.toDual 𝕜 F) f') s x

Alias of the forward direction of hasGradientWithinAt_iff_hasFDerivWithinAt.

theorem HasFDerivWithinAt.hasGradientWithinAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} {frechet : F →L[𝕜] 𝕜} {s : Set F} : HasFDerivWithinAt f frechet s x → HasGradientWithinAt f ((InnerProductSpace.toDual 𝕜 F).symm frechet) s x

Alias of the forward direction of hasFDerivWithinAt_iff_hasGradientWithinAt.

theorem HasGradientAt.hasFDerivAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} : HasGradientAt f f' x → HasFDerivAt f ((InnerProductSpace.toDual 𝕜 F) f') x

Alias of the forward direction of hasGradientAt_iff_hasFDerivAt.

theorem HasFDerivAt.hasGradientAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} {frechet : F →L[𝕜] 𝕜} : HasFDerivAt f frechet x → HasGradientAt f ((InnerProductSpace.toDual 𝕜 F).symm 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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} (h : ¬DifferentiableAt 𝕜 f x) : gradient f x = 0

theorem HasGradientAt.unique {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x gradf gradg : F} (hf : HasGradientAt f gradf x) (hg : HasGradientAt f gradg x) : gradf = gradg

theorem DifferentiableAt.hasGradientAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} (h : DifferentiableAt 𝕜 f x) : HasGradientAt f (gradient f x) x

theorem HasGradientAt.differentiableAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} (h : HasGradientAt f f' x) : DifferentiableAt 𝕜 f x

theorem DifferentiableWithinAt.hasGradientWithinAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} {s : Set F} (h : DifferentiableWithinAt 𝕜 f s x) : HasGradientWithinAt f (gradientWithin f s x) s x

theorem HasGradientWithinAt.differentiableWithinAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} (h : HasGradientWithinAt f f' s x) : DifferentiableWithinAt 𝕜 f s x

@[simp]

theorem hasGradientWithinAt_univ {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} : HasGradientWithinAt f f' Set.univ x ↔ HasGradientAt f f' x

theorem DifferentiableOn.hasGradientAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} {s : Set F} (h : DifferentiableOn 𝕜 f s) (hs : s ∈ nhds x) : HasGradientAt f (gradient f x) x

theorem HasGradientAt.gradient {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} (h : HasGradientAt f f' x) : _root_.gradient f x = f'

theorem gradient_eq {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' : F → F} (h : ∀ (x : F), HasGradientAt f (f' x) x) : gradient f = f'

theorem HasGradientAtFilter.hasDerivAtFilter {𝕜 : Type u_1} [RCLike 𝕜] {g : 𝕜 → 𝕜} {g' u : 𝕜} {L' : Filter 𝕜} (h : HasGradientAtFilter g g' u L') : HasDerivAtFilter g ((starRingEnd 𝕜) g') u L'

theorem HasDerivAtFilter.hasGradientAtFilter {𝕜 : Type u_1} [RCLike 𝕜] {g : 𝕜 → 𝕜} {g' u : 𝕜} {L' : Filter 𝕜} (h : HasDerivAtFilter g g' u L') : HasGradientAtFilter g ((starRingEnd 𝕜) g') u L'

theorem HasGradientAt.hasDerivAt {𝕜 : Type u_1} [RCLike 𝕜] {g : 𝕜 → 𝕜} {g' u : 𝕜} (h : HasGradientAt g g' u) : HasDerivAt g ((starRingEnd 𝕜) g') u

theorem HasDerivAt.hasGradientAt {𝕜 : Type u_1} [RCLike 𝕜] {g : 𝕜 → 𝕜} {g' u : 𝕜} (h : HasDerivAt g g' u) : HasGradientAt g ((starRingEnd 𝕜) g') u

theorem gradient_eq_deriv {𝕜 : Type u_1} [RCLike 𝕜] {g : 𝕜 → 𝕜} {u : 𝕜} : gradient g u = (starRingEnd 𝕜) (deriv g u)

theorem HasGradientAtFilter.hasDerivAtFilter' {g : ℝ → ℝ} {g' u : ℝ} {L' : Filter ℝ} (h : HasGradientAtFilter g g' u L') : HasDerivAtFilter g g' u L'

theorem HasDerivAtFilter.hasGradientAtFilter' {g : ℝ → ℝ} {g' u : ℝ} {L' : Filter ℝ} (h : HasDerivAtFilter g g' u L') : HasGradientAtFilter 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) : HasGradientAt 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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {L : Filter F} : 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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace 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[nhdsWithin x s] fun (x' : F) => x' - x

theorem hasGradientWithinAt_iff_tendsto {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace 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)‖) (nhdsWithin x s) (nhds 0)

theorem hasGradientAt_iff_isLittleO {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace 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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace 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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {L : Filter F} (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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {s t : Set F} (y : F) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) : HasGradientWithinAt f f' s x ↔ HasGradientWithinAt f f' t x

theorem hasGradientWithinAt_congr_set {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {s t : Set F} (h : s =ᶠ[nhds x] t) : HasGradientWithinAt f f' s x ↔ HasGradientWithinAt f f' t x

theorem hasGradientAt_iff_isLittleO_nhds_zero {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace 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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {x : F} {L : Filter F} {f₀ f₁ : F → 𝕜} {f₀' f₁' : F} (h₀ : f₀ =ᶠ[L] f₁) (hx : f₀ x = f₁ x) (h₁ : f₀' = f₁') : HasGradientAtFilter f₀ f₀' x L ↔ HasGradientAtFilter f₁ f₁' x L

theorem HasGradientAtFilter.congr_of_eventuallyEq {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {L : Filter F} {f₁ : F → 𝕜} (h : HasGradientAtFilter f f' x L) (hL : f₁ =ᶠ[L] f) (hx : f₁ x = f x) : HasGradientAtFilter f₁ f' x L

theorem HasGradientWithinAt.congr_mono {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} {f₁ : F → 𝕜} {t : Set F} (h : HasGradientWithinAt f f' s x) (ht : ∀ x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t ⊆ s) : HasGradientWithinAt f₁ f' t x

theorem HasGradientWithinAt.congr {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} {f₁ : F → 𝕜} (h : HasGradientWithinAt f f' s x) (hs : ∀ x ∈ s, f₁ x = f x) (hx : f₁ x = f x) : HasGradientWithinAt f₁ f' s x

theorem HasGradientWithinAt.congr_of_mem {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} {f₁ : F → 𝕜} (h : HasGradientWithinAt f f' s x) (hs : ∀ x ∈ s, f₁ x = f x) (hx : x ∈ s) : HasGradientWithinAt f₁ f' s x

theorem HasGradientWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} {f₁ : F → 𝕜} (h : HasGradientWithinAt f f' s x) (h₁ : f₁ =ᶠ[nhdsWithin x s] f) (hx : f₁ x = f x) : HasGradientWithinAt f₁ f' s x

theorem HasGradientWithinAt.congr_of_eventuallyEq_of_mem {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} {f₁ : F → 𝕜} (h : HasGradientWithinAt f f' s x) (h₁ : f₁ =ᶠ[nhdsWithin x s] f) (hx : x ∈ s) : HasGradientWithinAt f₁ f' s x

theorem HasGradientAt.congr_of_eventuallyEq {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {f₁ : F → 𝕜} (h : HasGradientAt f f' x) (h₁ : f₁ =ᶠ[nhds x] f) : HasGradientAt f₁ f' x

theorem Filter.EventuallyEq.gradient_eq {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} {f₁ : F → 𝕜} (hL : f₁ =ᶠ[nhds x] f) : gradient f₁ x = gradient f x

theorem Filter.EventuallyEq.gradient {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} {f₁ : F → 𝕜} (h : f₁ =ᶠ[nhds x] f) : gradient f₁ =ᶠ[nhds x] gradient f

The Gradient of constant functions

theorem hasGradientAtFilter_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (x : F) (L : Filter F) (c : 𝕜) : HasGradientAtFilter (fun (x : F) => c) 0 x L

theorem hasGradientWithinAt_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (x : F) (s : Set F) (c : 𝕜) : HasGradientWithinAt (fun (x : F) => c) 0 s x

theorem hasGradientAt_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (x : F) (c : 𝕜) : HasGradientAt (fun (x : F) => c) 0 x

theorem gradient_fun_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (x : F) (c : 𝕜) : gradient (fun (x : F) => c) x = 0

theorem gradient_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (x : F) (c : 𝕜) : gradient (Function.const F c) x = 0

@[simp]

theorem gradient_fun_const' {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (c : 𝕜) : (gradient fun (x : F) => c) = fun (x : F) => 0

@[simp]

theorem gradient_const' {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (c : 𝕜) : gradient (Function.const F c) = 0

Continuity of a function admitting a gradient

theorem HasGradientAtFilter.tendsto_nhds {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {L : Filter F} (hL : L ≤ nhds x) (h : HasGradientAtFilter f f' x L) : Filter.Tendsto f L (nhds (f x))

theorem HasGradientWithinAt.continuousWithinAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} (h : HasGradientWithinAt f f' s x) : ContinuousWithinAt f s x

theorem HasGradientAt.continuousAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' x : F} (h : HasGradientAt f f' x) : ContinuousAt f x

theorem HasGradientAt.continuousOn {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {s : Set F} {f' : F → F} (h : ∀ x ∈ s, HasGradientAt f (f' x) x) : ContinuousOn f s