Commit 2024-06-26 21:12 66c9c686

View on Github →

feat: the norm raised to a power is C^1 (#14124)

From the Sobolev inequality project
Generalize continuousAt_rpow_const

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Defs.lean

added theorem contDiff_one_iff_hasFDerivAt

Created Mathlib/Analysis/InnerProductSpace/NormPow.lean

added theorem ContDiff.norm_rpow

added theorem Differentiable.fderiv_norm_rpow

added theorem Differentiable.norm_rpow

added theorem contDiff_norm_rpow

added theorem differentiable_norm_rpow

added theorem fderiv_norm_rpow

added theorem hasDerivAt_abs_rpow

added theorem hasDerivAt_norm_rpow

added theorem hasFDerivAt_norm_rpow

added theorem nnnorm_fderiv_norm_rpow_le

added theorem norm_fderiv_norm_id_rpow

added theorem norm_fderiv_norm_rpow_le

Modified Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

modified theorem Real.continuousAt_rpow_const

added theorem Real.continuous_rpow_const

Modified Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

added theorem ENNReal.rpow_add_of_nonneg

added theorem NNReal.rpow_add_of_nonneg

added theorem Real.nnnorm_rpow_of_nonneg