Commit 2023-11-16 11:33 6d09b20c

View on Github →

feat: define gradient of scalar-valued function on a Hilbert space (#7074) This file describes the transformation of the fderiv to gradient for functions from H to ℝ, where H is a Hilbert (complete inner product) space. This is a substitution for the previous pull request #7011.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/Gradient/Basic.lean

added theorem DifferentiableAt.hasGradientAt

added theorem DifferentiableOn.hasGradientAt

added theorem DifferentiableWithinAt.hasGradientWithinAt

added theorem Filter.EventuallyEq.gradient_eq

added theorem Filter.EventuallyEq.hasGradientAtFilter_iff

added theorem HasDerivAt.hasGradientAt'

added theorem HasDerivAt.hasGradientAt

added theorem HasDerivAtFilter.hasGradientAtFilter'

added theorem HasDerivAtFilter.hasGradientAtFilter

added theorem HasGradientAt.congr_of_eventuallyEq

added theorem HasGradientAt.continuousAt

added theorem HasGradientAt.differentiableAt

added theorem HasGradientAt.gradient

added theorem HasGradientAt.hasDerivAt'

added theorem HasGradientAt.hasDerivAt

added theorem HasGradientAt.unique

added def HasGradientAt

added theorem HasGradientAtFilter.congr_of_eventuallyEq

added theorem HasGradientAtFilter.hasDerivAtFilter'

added theorem HasGradientAtFilter.hasDerivAtFilter

added theorem HasGradientAtFilter.isBigO_sub

added def HasGradientAtFilter

added theorem HasGradientWithinAt.congr

added theorem HasGradientWithinAt.congr_mono

added theorem HasGradientWithinAt.congr_of_eventuallyEq

added theorem HasGradientWithinAt.congr_of_eventuallyEq_of_mem

added theorem HasGradientWithinAt.congr_of_mem

added theorem HasGradientWithinAt.continuousWithinAt

added theorem HasGradientWithinAt.differentiableWithinAt

added def HasGradientWithinAt

added def gradient

added def gradientWithin

added theorem gradient_const'

added theorem gradient_const

added theorem gradient_eq

added theorem gradient_eq_deriv'

added theorem gradient_eq_deriv

added theorem gradient_eq_zero_of_not_differentiableAt

added theorem hasFDerivAt_iff_hasGradientAt

added theorem hasFDerivWithinAt_iff_hasGradientWithinAt

added theorem hasGradientAtFilter_const

added theorem hasGradientAtFilter_iff_isLittleO

added theorem hasGradientAt_const

added theorem hasGradientAt_iff_hasFDerivAt

added theorem hasGradientAt_iff_isLittleO

added theorem hasGradientAt_iff_isLittleO_nhds_zero

added theorem hasGradientAt_iff_tendsto

added theorem hasGradientWithinAt_congr_set'

added theorem hasGradientWithinAt_congr_set

added theorem hasGradientWithinAt_const

added theorem hasGradientWithinAt_iff_hasFDerivWithinAt

added theorem hasGradientWithinAt_iff_isLittleO

added theorem hasGradientWithinAt_iff_tendsto

added theorem hasGradientWithinAt_univ