Documentation

Mathlib.Analysis.Calculus.Gradient.Basic

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.

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

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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (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} [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
        Instances For
          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.

          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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F𝕜} {f' : F} {x : F} {s : Set F} :
              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' : F} {x : F} :
              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' : F} {x : F} {s : Set F} :

              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 xHasGradientWithinAt 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' : F} {x : F} :

              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 xHasGradientAt 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 : F} {gradf : F} {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) :
              theorem HasGradientAt.differentiableAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F𝕜} {f' : F} {x : F} (h : HasGradientAt f 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) :
              theorem HasGradientWithinAt.differentiableWithinAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {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) :
              theorem HasGradientAt.gradient {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F𝕜} {f' : F} {x : F} (h : HasGradientAt f f' x) :
              gradient f x = f'
              theorem gradient_eq {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F𝕜} {f' : FF} (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') :
              theorem HasDerivAtFilter.hasGradientAtFilter' {g : } {g' : } {u : } {L' : Filter } (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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {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' : 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' : 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' : 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' : 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' : 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' : 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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {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} {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' : F} {x : F} {L : Filter F} {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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {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} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {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) :
              theorem HasGradientWithinAt.congr_of_eventuallyEq_of_mem {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {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) :
              theorem HasGradientAt.congr_of_eventuallyEq {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {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) :

              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_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
              @[simp]
              theorem gradient_const' {𝕜 : Type u_1} [RCLike 𝕜] (c : 𝕜) :
              (gradient fun (x : 𝕜) => c) = fun (x : 𝕜) => 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' : 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' : F} {x : F} {s : Set F} (h : HasGradientWithinAt f f' s x) :
              theorem HasGradientAt.continuousAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F𝕜} {f' : F} {x : F} (h : HasGradientAt f 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' : FF} (h : xs, HasGradientAt f (f' x) x) :