Documentation

Mathlib.Analysis.Calculus.Deriv.Abs

Derivative of the absolute value #

This file compiles basic derivability properties of the absolute value, and is largely inspired from Mathlib.Analysis.InnerProductSpace.Calculus, which is the analogous file for norms derived from an inner product space.

Tags #

absolute value, derivative

source
theorem contDiffAt_abs {n : ℕ∞} {x : ℝ} (hx : x ≠ 0) :
ContDiffAt ℝ n (fun (x : ℝ) => |x|) x
source
theorem ContDiffAt.abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ∞} {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ n f x) (h₀ : f x ≠ 0) :
ContDiffAt ℝ n (fun (x : E) => |f x|) x
source
theorem contDiffWithinAt_abs {n : ℕ∞} {x : ℝ} (hx : x ≠ 0) (s : Set ℝ) :
ContDiffWithinAt ℝ n (fun (x : ℝ) => |x|) s x
source
theorem ContDiffWithinAt.abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ∞} {f : E → ℝ} {s : Set E} {x : E} (hf : ContDiffWithinAt ℝ n f s x) (h₀ : f x ≠ 0) :
ContDiffWithinAt ℝ n (fun (y : E) => |f y|) s x
source
theorem contDiffOn_abs {n : ℕ∞} {s : Set ℝ} (hs : ∀ x ∈ s, x ≠ 0) :
ContDiffOn ℝ n (fun (x : ℝ) => |x|) s
source
theorem ContDiffOn.abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ∞} {f : E → ℝ} {s : Set E} (hf : ContDiffOn ℝ n f s) (h₀ : ∀ x ∈ s, f x ≠ 0) :
ContDiffOn ℝ n (fun (y : E) => |f y|) s
source
theorem ContDiff.abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ∞} {f : E → ℝ} (hf : ContDiff ℝ n f) (h₀ : ∀ (x : E), f x ≠ 0) :
ContDiff ℝ n fun (y : E) => |f y|
source
theorem hasStrictDerivAt_abs_neg {x : ℝ} (hx : x < 0) :
HasStrictDerivAt (fun (x : ℝ) => |x|) (-1) x
source
theorem hasDerivAt_abs_neg {x : ℝ} (hx : x < 0) :
HasDerivAt (fun (x : ℝ) => |x|) (-1) x
source
theorem hasStrictDerivAt_abs_pos {x : ℝ} (hx : 0 < x) :
HasStrictDerivAt (fun (x : ℝ) => |x|) 1 x
source
theorem hasDerivAt_abs_pos {x : ℝ} (hx : 0 < x) :
HasDerivAt (fun (x : ℝ) => |x|) 1 x
source
theorem hasStrictDerivAt_abs {x : ℝ} (hx : x ≠ 0) :
HasStrictDerivAt (fun (x : ℝ) => |x|) (↑(SignType.sign x)) x
source
theorem hasDerivAt_abs {x : ℝ} (hx : x ≠ 0) :
HasDerivAt (fun (x : ℝ) => |x|) (↑(SignType.sign x)) x
source
theorem HasStrictFDerivAt.abs_of_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E} (hf : HasStrictFDerivAt f f' x) (h₀ : f x < 0) :
HasStrictFDerivAt (fun (x : E) => |f x|) (-f') x
source
theorem HasFDerivAt.abs_of_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E} (hf : HasFDerivAt f f' x) (h₀ : f x < 0) :
HasFDerivAt (fun (x : E) => |f x|) (-f') x
source
theorem HasStrictFDerivAt.abs_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E} (hf : HasStrictFDerivAt f f' x) (h₀ : 0 < f x) :
HasStrictFDerivAt (fun (x : E) => |f x|) f' x
source
theorem HasFDerivAt.abs_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E} (hf : HasFDerivAt f f' x) (h₀ : 0 < f x) :
HasFDerivAt (fun (x : E) => |f x|) f' x
source
theorem HasStrictFDerivAt.abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E} (hf : HasStrictFDerivAt f f' x) (h₀ : f x ≠ 0) :
HasStrictFDerivAt (fun (x : E) => |f x|) (↑(SignType.sign (f x)) • f') x
source
theorem HasFDerivAt.abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E} (hf : HasFDerivAt f f' x) (h₀ : f x ≠ 0) :
HasFDerivAt (fun (x : E) => |f x|) (↑(SignType.sign (f x)) • f') x
source
theorem hasDerivWithinAt_abs_neg (s : Set ℝ) {x : ℝ} (hx : x < 0) :
HasDerivWithinAt (fun (x : ℝ) => |x|) (-1) s x
source
theorem hasDerivWithinAt_abs_pos (s : Set ℝ) {x : ℝ} (hx : 0 < x) :
HasDerivWithinAt (fun (x : ℝ) => |x|) 1 s x
source
theorem hasDerivWithinAt_abs (s : Set ℝ) {x : ℝ} (hx : x ≠ 0) :
HasDerivWithinAt (fun (x : ℝ) => |x|) (↑(SignType.sign x)) s x
source
theorem HasFDerivWithinAt.abs_of_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {s : Set E} {x : E} (hf : HasFDerivWithinAt f f' s x) (h₀ : f x < 0) :
HasFDerivWithinAt (fun (x : E) => |f x|) (-f') s x
source
theorem HasFDerivWithinAt.abs_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {s : Set E} {x : E} (hf : HasFDerivWithinAt f f' s x) (h₀ : 0 < f x) :
HasFDerivWithinAt (fun (x : E) => |f x|) f' s x
source
theorem HasFDerivWithinAt.abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {s : Set E} {x : E} (hf : HasFDerivWithinAt f f' s x) (h₀ : f x ≠ 0) :
HasFDerivWithinAt (fun (x : E) => |f x|) (↑(SignType.sign (f x)) • f') s x
source
theorem differentiableAt_abs_neg {x : ℝ} (hx : x < 0) :
DifferentiableAt ℝ (fun (x : ℝ) => |x|) x
source
theorem differentiableAt_abs_pos {x : ℝ} (hx : 0 < x) :
DifferentiableAt ℝ (fun (x : ℝ) => |x|) x
source
theorem differentiableAt_abs {x : ℝ} (hx : x ≠ 0) :
DifferentiableAt ℝ (fun (x : ℝ) => |x|) x
source
theorem DifferentiableAt.abs_of_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) (h₀ : f x < 0) :
DifferentiableAt ℝ (fun (x : E) => |f x|) x
source
theorem DifferentiableAt.abs_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) (h₀ : 0 < f x) :
DifferentiableAt ℝ (fun (x : E) => |f x|) x
source
theorem DifferentiableAt.abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) (h₀ : f x ≠ 0) :
DifferentiableAt ℝ (fun (x : E) => |f x|) x
source
theorem differentiableWithinAt_abs_neg (s : Set ℝ) {x : ℝ} (hx : x < 0) :
DifferentiableWithinAt ℝ (fun (x : ℝ) => |x|) s x
source
theorem differentiableWithinAt_abs_pos (s : Set ℝ) {x : ℝ} (hx : 0 < x) :
DifferentiableWithinAt ℝ (fun (x : ℝ) => |x|) s x
source
theorem differentiableWithinAt_abs (s : Set ℝ) {x : ℝ} (hx : x ≠ 0) :
DifferentiableWithinAt ℝ (fun (x : ℝ) => |x|) s x
source
theorem DifferentiableWithinAt.abs_of_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E} (hf : DifferentiableWithinAt ℝ f s x) (h₀ : f x < 0) :
DifferentiableWithinAt ℝ (fun (x : E) => |f x|) s x
source
theorem DifferentiableWithinAt.abs_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E} (hf : DifferentiableWithinAt ℝ f s x) (h₀ : 0 < f x) :
DifferentiableWithinAt ℝ (fun (x : E) => |f x|) s x
source
theorem DifferentiableWithinAt.abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E} (hf : DifferentiableWithinAt ℝ f s x) (h₀ : f x ≠ 0) :
DifferentiableWithinAt ℝ (fun (x : E) => |f x|) s x
source
theorem differentiableOn_abs {s : Set ℝ} (hs : ∀ x ∈ s, x ≠ 0) :
DifferentiableOn ℝ (fun (x : ℝ) => |x|) s
source
theorem DifferentiableOn.abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (hf : DifferentiableOn ℝ f s) (h₀ : ∀ x ∈ s, f x ≠ 0) :
DifferentiableOn ℝ (fun (x : E) => |f x|) s
source
theorem Differentiable.abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : Differentiable ℝ f) (h₀ : ∀ (x : E), f x ≠ 0) :
Differentiable ℝ fun (x : E) => |f x|
source
theorem not_differentiableAt_abs_zero :
¬DifferentiableAt ℝ abs 0
source
theorem deriv_abs_neg {x : ℝ} (hx : x < 0) :
deriv (fun (x : ℝ) => |x|) x = -1
source
theorem deriv_abs_pos {x : ℝ} (hx : 0 < x) :
deriv (fun (x : ℝ) => |x|) x = 1
source
theorem deriv_abs_zero :
deriv (fun (x : ℝ) => |x|) 0 = 0
source
theorem deriv_abs (x : ℝ) :
deriv (fun (x : ℝ) => |x|) x = ↑(SignType.sign x)