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.

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

source

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

Instances For

source

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

Instances For

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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.

source

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.

source

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

source

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

source

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

source

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

source

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

source

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

source

@[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

source

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

source

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'

source

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'

source

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

HasDerivAtFilter g ((starRingEnd 𝕜) g') u L'

source

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

HasGradientAtFilter g ((starRingEnd 𝕜) g') u L'

source

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

HasDerivAt g ((starRingEnd 𝕜) g') u

source

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

HasGradientAt g ((starRingEnd 𝕜) g') u

source

theorem gradient_eq_deriv {𝕜 : Type u_1} [RCLike 𝕜] {g : 𝕜 → 𝕜} {u : 𝕜} :

gradient g u = (starRingEnd 𝕜) (deriv g u)

source

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

HasDerivAtFilter g g' u L'

source

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

HasGradientAtFilter g g' u L'

source

theorem HasGradientAt.hasDerivAt' {g : ℝ → ℝ} {g' u : ℝ} (h : HasGradientAt g g' u) :

HasDerivAt g g' u

source

theorem HasDerivAt.hasGradientAt' {g : ℝ → ℝ} {g' u : ℝ} (h : HasDerivAt g g' u) :

HasGradientAt g g' u

source

theorem gradient_eq_deriv' {g : ℝ → ℝ} {u : ℝ} :

gradient g u = deriv g u

source

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

source

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

source

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)

source

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

source

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)

source

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

source

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

source

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

source

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 #

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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 #

source

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

source

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

source

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

source

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

source

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

source

@[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

source

@[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 #

source

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))

source

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

source

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

source

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

Documentation

Mathlib.Analysis.Calculus.Gradient.Basic

Gradient #

Main Definitions #

Main results #

Congruence properties of the Gradient #

The Gradient of constant functions #

Continuity of a function admitting a gradient #