Derivative of the absolute value

This file compiles basic derivability properties of the absolute value, and is largely inspired from Mathlib/Analysis/InnerProductSpace/Calculus.lean, 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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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)