Commit 2023-06-05 02:03 d27c6251

View on Github →

feat: port Analysis.InnerProductSpace.Calculus (#4659)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/Calculus.lean

added theorem ContDiff.dist

added theorem ContDiff.inner

added theorem ContDiff.norm

added theorem ContDiff.norm_sq

added theorem ContDiffAt.dist

added theorem ContDiffAt.norm

added theorem ContDiffOn.dist

added theorem ContDiffOn.inner

added theorem ContDiffOn.norm

added theorem ContDiffOn.norm_sq

added theorem ContDiffWithinAt.dist

added theorem ContDiffWithinAt.inner

added theorem ContDiffWithinAt.norm

added theorem ContDiffWithinAt.norm_sq

added theorem Differentiable.dist

added theorem Differentiable.inner

added theorem Differentiable.norm

added theorem Differentiable.norm_sq

added theorem DifferentiableAt.dist

added theorem DifferentiableAt.inner

added theorem DifferentiableAt.norm

added theorem DifferentiableAt.norm_sq

added theorem DifferentiableOn.dist

added theorem DifferentiableOn.inner

added theorem DifferentiableOn.norm

added theorem DifferentiableOn.norm_sq

added theorem DifferentiableWithinAt.dist

added theorem DifferentiableWithinAt.inner

added theorem DifferentiableWithinAt.norm

added theorem DifferentiableWithinAt.norm_sq

added theorem HasDerivAt.inner

added theorem HasDerivWithinAt.inner

added theorem HasFDerivAt.inner

added theorem HasFDerivWithinAt.inner

added theorem HasStrictFDerivAt.inner

added theorem contDiffAt_euclidean

added theorem contDiffAt_inner

added theorem contDiffAt_norm

added theorem contDiffOn_euclidean

added theorem contDiffOn_homeomorphUnitBall_symm

added theorem contDiffWithinAt_euclidean

added theorem contDiff_euclidean

added theorem contDiff_homeomorphUnitBall

added theorem contDiff_inner

added theorem contDiff_norm_sq

added theorem deriv_inner_apply

added theorem differentiableAt_euclidean

added theorem differentiableOn_euclidean

added theorem differentiableWithinAt_euclidean

added theorem differentiable_euclidean

added theorem differentiable_inner

added def fderivInnerClm

added theorem fderivInnerClm_apply

added theorem fderiv_inner_apply

added theorem hasFDerivWithinAt_euclidean

added theorem hasStrictFDerivAt_euclidean

added theorem hasStrictFDerivAt_norm_sq