# Fréchet derivative of constant functions #

This file contains the usual formulas (and existence assertions) for the derivative of constant functions, including various special cases such as the functions `0`, `1`, `Nat.cast n`, `Int.cast z`, and other numerals.

## Tags #

derivative, differentiable, Fréchet, calculus

source
theorem hasStrictFDerivAt_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (c : F) (x : E) :
HasStrictFDerivAt (fun (x : E) => c) 0 x
source
theorem hasStrictFDerivAt_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) :
HasStrictFDerivAt 0 0 x
source
theorem hasStrictFDerivAt_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [One F] (x : E) :
HasStrictFDerivAt 1 0 x
source
theorem hasStrictFDerivAt_natCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NatCast F] (n : ℕ) (x : E) :
HasStrictFDerivAt (↑n) 0 x
source
theorem hasStrictFDerivAt_intCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IntCast F] (z : ℤ) (x : E) :
HasStrictFDerivAt (↑z) 0 x
source
theorem hasStrictFDerivAt_ofNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) [OfNat F n] (x : E) :
HasStrictFDerivAt (OfNat.ofNat n) 0 x
source
theorem hasFDerivAtFilter_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (c : F) (x : E) (L : Filter E) :
HasFDerivAtFilter (fun (x : E) => c) 0 x L
source
theorem hasFDerivAtFilter_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) (L : Filter E) :
HasFDerivAtFilter 0 0 x L
source
theorem hasFDerivAtFilter_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [One F] (x : E) (L : Filter E) :
HasFDerivAtFilter 1 0 x L
source
theorem hasFDerivAtFilter_natCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NatCast F] (n : ℕ) (x : E) (L : Filter E) :
HasFDerivAtFilter (↑n) 0 x L
source
theorem hasFDerivAtFilter_intCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IntCast F] (z : ℤ) (x : E) (L : Filter E) :
HasFDerivAtFilter (↑z) 0 x L
source
theorem hasFDerivAtFilter_ofNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) [OfNat F n] (x : E) (L : Filter E) :
HasFDerivAtFilter (OfNat.ofNat n) 0 x L
source
theorem hasFDerivWithinAt_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (c : F) (x : E) (s : Set E) :
HasFDerivWithinAt (fun (x : E) => c) 0 s x
source
theorem hasFDerivWithinAt_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) (s : Set E) :
HasFDerivWithinAt 0 0 s x
source
theorem hasFDerivWithinAt_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [One F] (x : E) (s : Set E) :
HasFDerivWithinAt 1 0 s x
source
theorem hasFDerivWithinAt_natCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NatCast F] (n : ℕ) (x : E) (s : Set E) :
HasFDerivWithinAt (↑n) 0 s x
source
theorem hasFDerivWithinAt_intCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IntCast F] (z : ℤ) (x : E) (s : Set E) :
HasFDerivWithinAt (↑z) 0 s x
source
theorem hasFDerivWithinAt_ofNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) [OfNat F n] (x : E) (s : Set E) :
HasFDerivWithinAt (OfNat.ofNat n) 0 s x
source
theorem hasFDerivAt_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (c : F) (x : E) :
HasFDerivAt (fun (x : E) => c) 0 x
source
theorem hasFDerivAt_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) :
HasFDerivAt 0 0 x
source
theorem hasFDerivAt_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [One F] (x : E) :
HasFDerivAt 1 0 x
source
theorem hasFDerivAt_natCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NatCast F] (n : ℕ) (x : E) :
HasFDerivAt (↑n) 0 x
source
theorem hasFDerivAt_intCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IntCast F] (z : ℤ) (x : E) :
HasFDerivAt (↑z) 0 x
source
theorem hasFDerivAt_ofNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) [OfNat F n] (x : E) :
HasFDerivAt (OfNat.ofNat n) 0 x
source
@[simp]
theorem differentiableAt_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (c : F) :
DifferentiableAt 𝕜 (fun (x : E) => c) x
source
@[simp]
theorem differentiableAt_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) :
DifferentiableAt 𝕜 0 x
source
@[simp]
theorem differentiableAt_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [One F] (x : E) :
DifferentiableAt 𝕜 1 x
source
@[simp]
theorem differentiableAt_natCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NatCast F] (n : ℕ) (x : E) :
DifferentiableAt 𝕜 (↑n) x
source
@[simp]
theorem differentiableAt_intCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IntCast F] (z : ℤ) (x : E) :
DifferentiableAt 𝕜 (↑z) x
source
@[simp]
theorem differentiableAt_ofNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) [OfNat F n] (x : E) :
DifferentiableAt 𝕜 (OfNat.ofNat n) x
source
theorem differentiableWithinAt_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (c : F) :
DifferentiableWithinAt 𝕜 (fun (x : E) => c) s x
source
theorem differentiableWithinAt_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} :
DifferentiableWithinAt 𝕜 0 s x
source
theorem differentiableWithinAt_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} [One F] :
DifferentiableWithinAt 𝕜 1 s x
source
theorem differentiableWithinAt_natCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} [NatCast F] (n : ℕ) :
DifferentiableWithinAt 𝕜 (↑n) s x
source
theorem differentiableWithinAt_intCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} [IntCast F] (z : ℤ) :
DifferentiableWithinAt 𝕜 (↑z) s x
source
theorem differentiableWithinAt_ofNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (n : ℕ) [OfNat F n] :
DifferentiableWithinAt 𝕜 (OfNat.ofNat n) s x
source
theorem fderivWithin_const_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (c : F) :
fderivWithin 𝕜 (fun (x : E) => c) s x = 0
source
@[simp]
theorem fderivWithin_fun_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (c : F) :
fderivWithin 𝕜 (fun (x : E) => c) s = 0
source
@[simp]
theorem fderivWithin_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (c : F) :
fderivWithin 𝕜 (Function.const E c) s = 0
source
@[simp]
theorem fderivWithin_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} :
fderivWithin 𝕜 0 s = 0
source
@[simp]
theorem fderivWithin_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} [One F] :
fderivWithin 𝕜 1 s = 0
source
@[simp]
theorem fderivWithin_natCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} [NatCast F] (n : ℕ) :
fderivWithin 𝕜 (↑n) s = 0
source
@[simp]
theorem fderivWithin_intCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} [IntCast F] (z : ℤ) :
fderivWithin 𝕜 (↑z) s = 0
source
@[simp]
theorem fderivWithin_ofNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (n : ℕ) [OfNat F n] :
fderivWithin 𝕜 (OfNat.ofNat n) s = 0
source
theorem fderiv_const_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (c : F) :
fderiv 𝕜 (fun (x : E) => c) x = 0
source
@[simp]
theorem fderiv_fun_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (c : F) :
(fderiv 𝕜 fun (x : E) => c) = 0
source
@[simp]
theorem fderiv_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (c : F) :
fderiv 𝕜 (Function.const E c) = 0
source
@[simp]
theorem fderiv_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
fderiv 𝕜 0 = 0
source
@[simp]
theorem fderiv_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [One F] :
fderiv 𝕜 1 = 0
source
@[simp]
theorem fderiv_natCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NatCast F] (n : ℕ) :
fderiv 𝕜 ↑n = 0
source
@[simp]
theorem fderiv_intCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IntCast F] (z : ℤ) :
fderiv 𝕜 ↑z = 0
source
@[simp]
theorem fderiv_ofNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) [OfNat F n] :
fderiv 𝕜 (OfNat.ofNat n) = 0
source
@[simp]
theorem differentiable_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (c : F) :
Differentiable 𝕜 fun (x : E) => c
source
@[simp]
theorem differentiable_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
Differentiable 𝕜 0
source
@[simp]
theorem differentiable_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [One F] :
Differentiable 𝕜 1
source
@[simp]
theorem differentiable_natCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NatCast F] (n : ℕ) :
Differentiable 𝕜 ↑n
source
@[simp]
theorem differentiable_intCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IntCast F] (z : ℤ) :
Differentiable 𝕜 ↑z
source
@[simp]
theorem differentiable_ofNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) [OfNat F n] :
Differentiable 𝕜 (OfNat.ofNat n)
source
@[simp]
theorem differentiableOn_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (c : F) :
DifferentiableOn 𝕜 (fun (x : E) => c) s
source
@[simp]
theorem differentiableOn_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} :
DifferentiableOn 𝕜 0 s
source
@[simp]
theorem differentiableOn_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} [One F] :
DifferentiableOn 𝕜 1 s
source
@[simp]
theorem differentiableOn_natCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} [NatCast F] (n : ℕ) :
DifferentiableOn 𝕜 (↑n) s
source
@[simp]
theorem differentiableOn_intCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} [IntCast F] (z : ℤ) :
DifferentiableOn 𝕜 (↑z) s
source
@[simp]
theorem differentiableOn_ofNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (n : ℕ) [OfNat F n] :
DifferentiableOn 𝕜 (OfNat.ofNat n) s
source
theorem hasFDerivWithinAt_singleton {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (x : E) :
HasFDerivWithinAt f 0 {x} x
source
theorem hasFDerivAt_of_subsingleton {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [h : Subsingleton E] (f : E → F) (x : E) :
HasFDerivAt f 0 x
source
theorem differentiableOn_empty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} :
DifferentiableOn 𝕜 f ∅
source
theorem differentiableOn_singleton {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} :
DifferentiableOn 𝕜 f {x}
source
theorem Set.Subsingleton.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hs : s.Subsingleton) :
DifferentiableOn 𝕜 f s
source
theorem hasFDerivAt_zero_of_eventually_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (c : F) (hf : f =ᶠ[nhds x] fun (x : E) => c) :
HasFDerivAt f 0 x
source
theorem differentiableWithinAt_of_isInvertible_fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} (hf : (fderivWithin 𝕜 f s x).IsInvertible) :
DifferentiableWithinAt 𝕜 f s x
source
theorem differentiableAt_of_isInvertible_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (hf : (fderiv 𝕜 f x).IsInvertible) :
DifferentiableAt 𝕜 f x

### Support of derivatives #

source
theorem HasStrictFDerivAt.of_notMem_tsupport (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : x ∉ tsupport f) :
HasStrictFDerivAt f 0 x
source
@[deprecated HasStrictFDerivAt.of_notMem_tsupport (since := "2025-05-24")]
theorem HasStrictFDerivAt.of_nmem_tsupport (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : x ∉ tsupport f) :
HasStrictFDerivAt f 0 x

Alias of `HasStrictFDerivAt.of_notMem_tsupport`.

source
theorem HasFDerivAt.of_notMem_tsupport (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : x ∉ tsupport f) :
HasFDerivAt f 0 x
source
@[deprecated HasFDerivAt.of_notMem_tsupport (since := "2025-05-24")]
theorem HasFDerivAt.of_nmem_tsupport (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : x ∉ tsupport f) :
HasFDerivAt f 0 x

Alias of `HasFDerivAt.of_notMem_tsupport`.

source
theorem HasFDerivWithinAt.of_notMem_tsupport (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E} (h : x ∉ tsupport f) :
HasFDerivWithinAt f 0 s x
source
@[deprecated HasFDerivWithinAt.of_notMem_tsupport (since := "2025-05-23")]
theorem HasFDerivWithinAt.of_not_mem_tsupport (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E} (h : x ∉ tsupport f) :
HasFDerivWithinAt f 0 s x

Alias of `HasFDerivWithinAt.of_notMem_tsupport`.

source
theorem fderiv_of_notMem_tsupport (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : x ∉ tsupport f) :
fderiv 𝕜 f x = 0
source
@[deprecated fderiv_of_notMem_tsupport (since := "2025-05-23")]
theorem fderiv_of_not_mem_tsupport (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : x ∉ tsupport f) :
fderiv 𝕜 f x = 0

Alias of `fderiv_of_notMem_tsupport`.

source
theorem support_fderiv_subset (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} :
Function.support (fderiv 𝕜 f) ⊆ tsupport f
source
theorem tsupport_fderiv_subset (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} :
tsupport (fderiv 𝕜 f) ⊆ tsupport f
source
theorem HasCompactSupport.fderiv (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (hf : HasCompactSupport f) :
HasCompactSupport (fderiv 𝕜 f)
source
theorem HasCompactSupport.fderiv_apply (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (hf : HasCompactSupport f) (v : E) :
HasCompactSupport fun (x : E) => (fderiv 𝕜 f x) v