Documentation

Mathlib.Analysis.Calculus.FDeriv.Const

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