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

theorem contDiffAt_abs {n : ℕ∞} {x : ℝ} (hx : x ≠ 0) : ContDiffAt ℝ (↑n) (fun (x : ℝ) => |x|) x

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

theorem contDiffWithinAt_abs {n : ℕ∞} {x : ℝ} (hx : x ≠ 0) (s : Set ℝ) : ContDiffWithinAt ℝ (↑n) (fun (x : ℝ) => |x|) s x

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

theorem contDiffOn_abs {n : ℕ∞} {s : Set ℝ} (hs : ∀ x ∈ s, x ≠ 0) : ContDiffOn ℝ (↑n) (fun (x : ℝ) => |x|) s

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

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|

theorem hasStrictDerivAt_abs_neg {x : ℝ} (hx : x < 0) : HasStrictDerivAt (fun (x : ℝ) => |x|) (-1) x

theorem hasDerivAt_abs_neg {x : ℝ} (hx : x < 0) : HasDerivAt (fun (x : ℝ) => |x|) (-1) x

theorem hasStrictDerivAt_abs_pos {x : ℝ} (hx : 0 < x) : HasStrictDerivAt (fun (x : ℝ) => |x|) 1 x

theorem hasDerivAt_abs_pos {x : ℝ} (hx : 0 < x) : HasDerivAt (fun (x : ℝ) => |x|) 1 x

theorem hasStrictDerivAt_abs {x : ℝ} (hx : x ≠ 0) : HasStrictDerivAt (fun (x : ℝ) => |x|) (↑(SignType.sign x)) x

theorem hasDerivAt_abs {x : ℝ} (hx : x ≠ 0) : HasDerivAt (fun (x : ℝ) => |x|) (↑(SignType.sign x)) x

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

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

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

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

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

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

theorem hasDerivWithinAt_abs_neg (s : Set ℝ) {x : ℝ} (hx : x < 0) : HasDerivWithinAt (fun (x : ℝ) => |x|) (-1) s x

theorem hasDerivWithinAt_abs_pos (s : Set ℝ) {x : ℝ} (hx : 0 < x) : HasDerivWithinAt (fun (x : ℝ) => |x|) 1 s x

theorem hasDerivWithinAt_abs (s : Set ℝ) {x : ℝ} (hx : x ≠ 0) : HasDerivWithinAt (fun (x : ℝ) => |x|) (↑(SignType.sign x)) s x

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

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

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

theorem differentiableAt_abs_neg {x : ℝ} (hx : x < 0) : DifferentiableAt ℝ (fun (x : ℝ) => |x|) x

theorem differentiableAt_abs_pos {x : ℝ} (hx : 0 < x) : DifferentiableAt ℝ (fun (x : ℝ) => |x|) x

theorem differentiableAt_abs {x : ℝ} (hx : x ≠ 0) : DifferentiableAt ℝ (fun (x : ℝ) => |x|) x

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

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

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

theorem differentiableWithinAt_abs_neg (s : Set ℝ) {x : ℝ} (hx : x < 0) : DifferentiableWithinAt ℝ (fun (x : ℝ) => |x|) s x

theorem differentiableWithinAt_abs_pos (s : Set ℝ) {x : ℝ} (hx : 0 < x) : DifferentiableWithinAt ℝ (fun (x : ℝ) => |x|) s x

theorem differentiableWithinAt_abs (s : Set ℝ) {x : ℝ} (hx : x ≠ 0) : DifferentiableWithinAt ℝ (fun (x : ℝ) => |x|) s x

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

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

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

theorem differentiableOn_abs {s : Set ℝ} (hs : ∀ x ∈ s, x ≠ 0) : DifferentiableOn ℝ (fun (x : ℝ) => |x|) s

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

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|

theorem not_differentiableAt_abs_zero : ¬DifferentiableAt ℝ abs 0

theorem deriv_abs_neg {x : ℝ} (hx : x < 0) : deriv (fun (x : ℝ) => |x|) x = -1

theorem deriv_abs_pos {x : ℝ} (hx : 0 < x) : deriv (fun (x : ℝ) => |x|) x = 1

theorem deriv_abs_zero : deriv (fun (x : ℝ) => |x|) 0 = 0

theorem deriv_abs (x : ℝ) : deriv (fun (x : ℝ) => |x|) x = ↑(SignType.sign x)