Gradient.division

Main results

This file contains the division parts of gradient, which can't be found in fderiv.

As the functions discussed in this file are restricted to E → ℝ

Two main theorems are formalized in this file

• HasGradientAt.one_div, shows the gradient at x of 1 / f x where f x ≠ 0.
• HasGradientAt.div, shows the gradient at x of f x / g x where g x ≠ 0.

theorem Vert_abs (a : ℝ) (b : ℝ) : ‖|a| - |b|‖ ≤ ‖a - b‖

theorem Vert_div (a : ℝ) (b : ℝ) : ‖a / b‖ = ‖a‖ * ‖1 / b‖

theorem Simplifying₁ (a : ℝ) (b : ℝ) (h₁ : a ≠ 0) (h₂ : b ≠ 0) (h₃ : ‖b‖ / 2 ≤ ‖a‖) : ‖1 / (b * b * a)‖ ≤ ‖2 / (b * b * b)‖

theorem Simplifying₂ (a : ℝ) (b : ℝ) (c : ℝ) (d : ℝ) (h₁ : a ≠ 0) (h₂ : 0 ≤ c) : ‖2 / (a * a * a)‖ * b * (c + 1) * (d * ‖a‖ * ‖a‖ * ‖a‖ / (4 * (c + 1))) = d / 2 * b

theorem div_div_mul (a : ℝ) (b : ℝ) (c : ℝ) (h₁ : a / b ≤ c) (h₂ : 0 < a) (h₃ : 0 < b) (h₄ : 0 < c) : 1 / c ≤ b / a

theorem HasGradientAt.one_div {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {grad : E} (hf : HasGradientAt f grad x) (h₁ : ¬f x = 0) : HasGradientAt (fun (y : E) => 1 / f y) (-(1 / f x ^ 2) • grad) x