/- Copyright (c) 2023 Chenyi Li. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Chenyi Li, Ziyu Wang, Penghao Yu, Zhipeng Cao, Zaiwen Wen -/ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Analysis.Calculus.MeanValue import Mathlib.Analysis.InnerProductSpace.Dual import Mathlib.Analysis.Calculus.Gradient.Basic import Optlib.Convex.ConvexFunction import Optlib.Differential.Lemmas /-! # 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`. -/ variable (a b c d : ℝ) variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] variable {f : E → ℝ} {f' : E → E} {x y : E} {s : Set E} variable {x y grad x': E} {gradient' : E} local notation "⟪" x ", " y "⟫" => @inner ℝ _ _ x y lemma Vert_abs : ‖|a| - |b|‖ ≤ ‖a - b‖ := by simp only [Real.norm_eq_abs] exact abs_abs_sub_abs_le_abs_sub a b lemma Vert_div : ‖a / b‖ = ‖a‖ * ‖1 / b‖ := by simp only [norm_div, Real.norm_eq_abs, one_div, norm_inv] exact rfl lemma Simplifying₁ (h₁ : a ≠ 0) (h₂ : b ≠ 0) (h₃ : ‖b‖ / 2 ≤ ‖a‖) : ‖1 / (b * b * a)‖ ≤ ‖2 / (b * b * b)‖ := by rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_div, abs_div] rw [Real.norm_eq_abs, Real.norm_eq_abs] at h₃ have l₁ : |1| / |b * b * a| = 1 / |b * b * a| := by norm_num have l₂ : |2| / |b * b * b| = 1 / (|b * b * b| / 2) := by norm_num rw [l₁, l₂, ← le_one_div] simp only [one_div, div_inv_eq_mul, one_mul] have l₃ : |b * b * b| / 2 = |b * b| * (|b| / 2) := by rw [mul_div, abs_mul] have l₄ : |b * b * a| = |b * b| * |a| := by rw [abs_mul] rw [l₃, l₄, mul_le_mul_left] apply h₃ rw [abs_pos] simp only [ne_eq, mul_eq_zero, or_self] apply h₂ have : 0 < |b * b * b| := by rw [abs_pos]; simp [h₂] have : 0 < |b * b * b| / 2 := half_pos this apply this have : 0 < |b * b * a| := by rw [abs_pos]; simp [h₁, h₂] exact Iff.mpr one_div_pos this lemma Simplifying₂ (h₁ : a ≠ 0) (h₂ : 0 ≤ c) : ‖(2 / (a * a * a))‖ * b * (c + 1) * (d * ‖a‖ * ‖a‖ * ‖a‖ / (4 * (c + 1))) = (d / 2) * b := by have l₁: |(2 / (a * a * a))| = |2| / |a * a * a| := norm_div 2 (a * a * a) have l₂: d * ‖a‖ * ‖a‖ * ‖a‖ = d * |a * a * a| := by repeat rw [Real.norm_eq_abs]; rw [abs_mul, abs_mul, ← mul_assoc, ← mul_assoc] have l₃: (c + 1) * (d * |a * a * a| / (4 * (c + 1))) = (d * |a * a * a| / 4) := by have : d * |a * a * a| / (4 * (c + 1)) = (d * |a * a * a| / 4) / (c + 1):= by exact div_mul_eq_div_div (d * |a * a * a|) _ _ rw [mul_comm, this] apply div_mul_cancel₀ linarith have l₄ : |2| / |a * a * a| * b * |a * a * a| = |2| * b := by rw [mul_comm (|2| / |a * a * a|), mul_assoc, div_mul_cancel₀, mul_comm] simp only [ne_eq, abs_eq_zero, mul_eq_zero, or_self] apply h₁ rw [Real.norm_eq_abs, l₁, l₂, mul_assoc,l₃, mul_comm d, ← mul_div, ← mul_assoc, l₄] norm_num; ring_nf lemma div_div_mul (h₁ : a / b ≤ c) (h₂ : 0 < a) (h₃ : 0 < b) (h₄ : 0 < c): 1 / c ≤ b / a := by have : a ≤ c * b := Iff.mp (div_le_iff₀ h₃) h₁ have : a ≤ b * c := by linarith apply Iff.mpr (div_le_div_iff h₄ h₂) rw [one_mul] apply this theorem HasGradientAt.one_div (hf : HasGradientAt f grad x)(h₁: ¬ f x = (0 : ℝ)): HasGradientAt (fun y => (1 : ℝ) / (f y)) (- ((1 : ℝ) / (f x) ^ (2 : ℕ)) • grad) x := by have hf' : HasGradientAt f grad x := hf rw [HasGradient_iff_Convergence_Point] intro ε εpos rcases (ContinuousAt_Convergence (ContinuousAt.abs (HasGradientAt.continuousAt hf))) ε εpos with ⟨δ', _ , _⟩ have ε1pos : 0 < ε * ‖f x‖ * ‖f x‖ / 4 := by apply div_pos repeat apply mul_pos apply εpos repeat apply Iff.mpr norm_pos_iff h₁ norm_num have h₀ : ∃ δ₀ > (0 : ℝ), ∀ (x' : E), ‖x - x'‖ ≤ δ₀ → ‖f x‖ / 2 ≤ ‖f x'‖ := by have absh : ∃ δ₀ > (0 : ℝ), ∀ (x' : E), ‖x - x'‖ ≤ δ₀ → ‖|f x'| - |f x|‖ ≤ ‖f x‖ / 2 := by apply (ContinuousAt_Convergence (ContinuousAt.abs (HasGradientAt.continuousAt hf))) apply div_pos apply Iff.mpr norm_pos_iff h₁ norm_num have absh' : ∃ δ₀ > (0 : ℝ), ∀ (x' : E), ‖x - x'‖ ≤ δ₀ → |f x| - ‖f x‖/2 ≤ ‖f x'‖ := by rcases absh with ⟨δ₀, δ₀pos, so⟩ use δ₀ constructor apply δ₀pos intro x' h specialize so x' h exact sub_le_of_abs_sub_le_left so have equal : |f x| - ‖f x‖/2 = ‖f x‖/2 := by exact sub_half |f x| rw [equal] at absh' apply absh' rcases h₀ with ⟨δ₀, δ₀pos, hδ₀⟩ rw [HasGradient_iff_Convergence_Point] at hf rcases hf (ε * ‖f x‖ * ‖f x‖ /4) ε1pos with ⟨δ'',δ''pos,hm2⟩ have h₂ : ∃ δ₂ > (0 : ℝ ), ∀ (x' : E), ‖x - x'‖ ≤ δ₂ → ‖f x - f x' + ⟪grad, (x' - x)⟫‖ ≤ ε * ‖f x‖ * ‖f x‖/4 * ‖x - x'‖ := by use δ'' constructor apply δ''pos intro x' h' have sep2 : ∀ (x' : E), ‖x - x'‖ ≤ δ'' → ‖f x - f x' + ⟪grad, (x' - x)⟫‖ ≤ ε * ‖f x‖ * ‖f x‖/4 * ‖x - x'‖ := by intro x1 hp1 specialize hm2 x1 hp1 have hp' : ‖f x - f x1 + ⟪grad, (x1 - x)⟫‖ = ‖f x1 - f x - ⟪grad, (x1 - x)⟫‖ := by have h'' : f x - f x1 + ⟪grad, (x1 - x)⟫ = - (f x1 - f x - ⟪grad, (x1 - x)⟫) := by linarith rw [h''] apply norm_neg rw [← hp'] at hm2 apply hm2 specialize sep2 x' h' apply sep2 rcases h₂ with ⟨δ₂, δ₂pos, hδ₂⟩ have ε2pos : 0 < ε * ‖f x‖ * ‖f x‖ * ‖f x‖ /(4 * (‖grad‖ + 1 )) := by apply div_pos repeat apply mul_pos apply εpos apply Iff.mpr norm_pos_iff h₁ apply Iff.mpr norm_pos_iff h₁ norm_num apply h₁ apply mul_pos linarith have h' : (0 : ℝ) < 1 := by linarith have h'' : 0 ≤ ‖grad‖ := by exact norm_nonneg (grad) exact add_pos_of_nonneg_of_pos h'' h' have h₃ : ∃ δ₃ > (0 : ℝ), ∀ (x' : E), ‖x - x'‖ ≤ δ₃ → ‖f x' - f x‖ ≤ ε * ‖f x‖ * ‖f x‖ * ‖f x‖ /(4 * (‖grad‖ + 1 )) := by apply ContinuousAt_Convergence · exact HasGradientAt.continuousAt hf' · exact ε2pos rcases h₃ with ⟨δ₃,δ₃pos,hδ₃⟩ have h₄ : ∃ δ > (0 : ℝ ), ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖(f x' * ⟪grad, (x' - x)⟫ - f x * ⟪grad, (x' - x)⟫)/((f x) * (f x) * (f x'))‖ ≤ (ε / 2) * ‖x' - x‖ := by use min δ₀ δ₃ constructor exact lt_min δ₀pos δ₃pos intro x' h' have hp₁ : ‖x - x'‖ ≤ δ₀ := by have h₂ : min δ₀ δ₃ ≤ δ₀ := by exact min_le_left δ₀ δ₃ apply le_trans h' h₂ have hp₂ : ‖x - x'‖ ≤ δ₃ := by have h₂ : min δ₀ δ₃ ≤ δ₃ := by exact min_le_right δ₀ δ₃ apply le_trans h' h₂ have l0 : 0 < ‖f x'‖ := by have h' : ‖f x‖/2 ≤ ‖f x'‖ := hδ₀ x' hp₁ have h'' : 0 < ‖f x‖/2 := by apply div_pos apply Iff.mpr norm_pos_iff h₁ norm_num apply lt_of_lt_of_le h'' h' have l1 : ‖(f x' - f x) * ⟪grad, (x' - x)⟫/((f x) * (f x) * (f x'))‖ = ‖(f x' - f x) * ⟪grad, (x' - x)⟫‖ * ‖1 / ((f x) * (f x) * (f x'))‖ := by apply Vert_div have l2 : ‖(f x' - f x) * ⟪grad, (x' - x)⟫‖ * ‖1 / ((f x) * (f x) * (f x'))‖ = ‖f x' - f x‖ * ‖ ⟪grad, (x' - x)⟫‖ * ‖1 / ((f x) * (f x) * (f x'))‖ := by have h' : ‖(f x' - f x) * ⟪grad, (x' - x)⟫‖ = ‖f x' - f x‖ * ‖ ⟪grad, (x' - x)⟫‖ := by exact norm_mul (f x' - f x) ⟪grad, (x' - x)⟫ rw [h'] have l3 : ‖f x' - f x‖ * ‖⟪grad, (x' - x)⟫‖ ≤ ‖f x' - f x‖ * ‖grad‖ * ‖x' - x‖ := by have h' : ‖f x' - f x‖ * ‖grad‖ * ‖x' - x‖ = ‖f x' - f x‖ * (‖grad‖ * ‖x' - x‖) := by apply mul_assoc rw [h'] have h'' : 0 ≤ ‖f x' - f x‖ := by apply norm_nonneg (f x' - f x) have h''' : ‖⟪grad, (x' - x)⟫‖ ≤ ‖grad‖ * ‖x' - x‖ := by exact norm_inner_le_norm grad (x' - x) exact mul_le_mul_of_nonneg_left h''' h'' have l5 : ‖f x' - f x‖ ≤ ε * ‖f x‖ * ‖f x‖ * ‖f x‖ /(4 * (‖grad‖ + 1 )) := hδ₃ x' hp₂ calc ‖(f x' * ⟪grad, (x' - x)⟫ - f x * ⟪grad, (x' - x)⟫)/(f x * f x * f x')‖ = ‖(f x' - f x) * ⟪grad, (x' - x)⟫/((f x) * (f x) * (f x'))‖ := by rw [← sub_mul] _ = ‖(f x' - f x) * ⟪grad, (x' - x)⟫‖ * ‖1 / ((f x) * (f x) * (f x'))‖ := l1 _ = ‖f x' - f x‖ * ‖⟪grad, (x' - x)⟫‖ * ‖1 / ((f x) * (f x) * (f x'))‖ := l2 _ ≤ ‖f x' - f x‖ * ‖grad‖ * ‖x' - x‖ * ‖1 / ((f x) * (f x) * (f x'))‖ := by have h' : 0 ≤ ‖1 / ((f x) * (f x) * (f x'))‖ := by apply norm_nonneg (1 / ((f x) * (f x) * (f x'))) apply mul_le_mul_of_nonneg_right l3 h' _ ≤ ‖(f x' - f x)‖ * ‖grad‖ * ‖x' - x‖ * ‖2 / ((f x) * (f x) * (f x))‖ := by have h'' : ‖1 / ((f x) * (f x) * (f x'))‖ ≤ ‖2 / ((f x) * (f x) * (f x))‖ := by apply Simplifying₁ (f x') (f x) apply Iff.mp norm_pos_iff l0 apply h₁ apply hδ₀ apply hp₁ exact mul_le_mul_of_nonneg_left h'' (mul_nonneg (mul_nonneg (norm_nonneg (f x' - f x)) (norm_nonneg grad)) (norm_nonneg (x' - x))) _ ≤ ‖(2 / ((f x) * (f x) * (f x)))‖ * ‖f x' - f x‖ * ‖x' - x‖ * ‖grad‖ := by linarith _ ≤ ‖(2 / ((f x) * (f x) * (f x)))‖ * ‖f x' - f x‖ * ‖x' - x‖ * (‖grad‖ + 1) := by have h' : ‖grad‖ ≤ ‖grad‖ + 1 := by linarith exact mul_le_mul_of_nonneg_left h' (mul_nonneg (mul_nonneg (norm_nonneg (2 / (f x * f x * f x))) (norm_nonneg (f x' - f x))) (norm_nonneg (x' - x))) _ = ‖(2 / ((f x) * (f x) * (f x)))‖ * ‖x' - x‖ * (‖grad‖ + 1) * ‖f x' - f x‖ := by linarith _ ≤ ‖(2 / ((f x) * (f x) * (f x)))‖ * ‖x' - x‖ * (‖grad‖ + 1) * (ε * ‖f x‖ * ‖f x‖ * ‖f x‖ /(4 * (‖grad‖ + 1 ))) := by apply mul_le_mul_of_nonneg_left l5 apply mul_nonneg apply mul_nonneg apply norm_nonneg apply norm_nonneg have h' : 0 ≤ ‖grad‖ := by apply norm_nonneg have h'' : ‖grad‖ ≤ ‖grad‖ + 1 := by linarith apply le_trans h' h'' _ = (ε / 2) * ‖x' - x‖ := by apply Simplifying₂ apply h₁ apply norm_nonneg rcases h₄ with ⟨δ₄,δ₄pos,hδ₄⟩ have h₅ : ∃ δ > (0 : ℝ ), ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖f x * (f x -f x' + ⟪grad, (x' - x)⟫)/((f x) * (f x) * (f x'))‖ ≤ (ε / 2) * ‖x' - x‖ := by use min δ₀ δ₂ constructor exact lt_min δ₀pos δ₂pos intro x' h' have hp₁ : ‖x - x'‖ ≤ δ₀ := by have h₂ : min δ₀ δ₂ ≤ δ₀ := by exact min_le_left δ₀ δ₂ apply le_trans h' h₂ have hp₂ : ‖x - x'‖ ≤ δ₂ := by have h₂ : min δ₀ δ₂ ≤ δ₂ := by exact min_le_right δ₀ δ₂ apply le_trans h' h₂ have zp1 :‖f x * (f x - f x' + inner grad (x' - x)) / (f x * f x * f x')‖ = ‖(f x - f x' + inner grad (x' - x)) / (f x * f x')‖ := by rw [mul_comm, mul_assoc (f x) (f x) (f x'), div_mul_eq_div_div ((f x - f x' + inner grad (x' - x)) * (f x)) (f x) (f x * f x'), mul_div_cancel_right₀] apply h₁ have zp2 : ‖f x‖ * ‖f x‖/2 ≤ ‖f x * f x'‖ := by have h' : ‖f x * f x'‖ = ‖f x‖ * ‖f x'‖ := by exact norm_mul (f x) (f x') rw [h'] have h'' : ‖f x‖ * ‖f x‖/2 = ‖f x‖ * ‖f x‖ * (1/2) := by linarith rw [h''] rw [mul_assoc] apply mul_le_mul_of_nonneg_left have h''' : ‖f x‖ * (1/2) = ‖f x‖/2 := by linarith rw [h'''] apply hδ₀ apply hp₁ apply norm_nonneg have zp3 : ‖1/(f x * f x')‖ ≤ 2 / (‖f x‖ * ‖f x‖) := by have zp4 : 1 / ‖f x * f x'‖ = ‖1/(f x * f x')‖ := by have h₁ : (0 : ℝ) ≤ (1 : ℝ) := by exact zero_le_one have h' : 1 = ‖(1 : ℝ)‖ := by exact Eq.symm (Real.norm_of_nonneg h₁) nth_rw 1 [h'] exact Eq.symm (norm_div 1 (f x * f x')) rw [← zp4] apply div_div_mul (‖f x‖ * ‖f x‖) 2 ‖f x * f x'‖ apply zp2 apply mul_pos apply Iff.mpr norm_pos_iff h₁ apply Iff.mpr norm_pos_iff h₁ norm_num rw [norm_mul] apply mul_pos apply Iff.mpr norm_pos_iff h₁ have h' : ‖f x‖/2 ≤ ‖f x'‖ := hδ₀ x' hp₁ have h'' : 0 < ‖f x‖/2 := by apply div_pos apply Iff.mpr norm_pos_iff h₁ norm_num apply lt_of_lt_of_le h'' h' have zp5 : ((ε * ‖f x‖ * ‖f x‖ / 4) * ‖x - x'‖) * (2 / (‖f x‖ * ‖f x‖)) = (ε / 2) * ‖x' - x‖ := by have l : ‖f x‖ ≠ 0 := by exact Iff.mpr norm_ne_zero_iff h₁ calc ((ε * ‖f x‖ * ‖f x‖/4) * ‖x - x'‖) * (2 / (‖f x‖ * ‖f x‖)) = (ε / 2) * ‖x - x'‖ * ((‖f x‖ * ‖f x‖)/(‖f x‖ * ‖f x‖)) := by ring_nf _ = (ε / 2) * ‖x' - x‖ := by rw [div_self (mul_ne_zero l l), mul_one, norm_sub_rev] calc ‖f x * (f x - f x' + inner grad (x' - x)) / (f x * f x * f x')‖ = ‖(f x - f x' + inner grad (x' - x)) / (f x * f x')‖ := by apply zp1 _ = ‖(f x - f x' + inner grad (x' - x))‖ * ‖1/(f x * f x')‖ := by apply Vert_div _ ≤ ‖(f x - f x' + inner grad (x' - x))‖ * (2 / (‖f x‖ * ‖f x‖)) := by apply mul_le_mul_of_nonneg_left zp3 apply norm_nonneg _ ≤ ((ε * ‖f x‖ * ‖f x‖/4) * ‖x - x'‖) * (2 / (‖f x‖ * ‖f x‖)) := by have : ‖(f x - f x' + inner grad (x' - x))‖ ≤ (ε * ‖f x‖ * ‖f x‖/4) * ‖x - x'‖ := by apply hδ₂ apply hp₂ apply mul_le_mul_of_nonneg_right this apply div_nonneg norm_num apply mul_nonneg apply norm_nonneg apply norm_nonneg _ = (ε / 2) * ‖x' - x‖ := by apply zp5 rcases h₅ with ⟨δ₅,δ₅pos,hδ₅⟩ use min δ₀ (min δ₄ δ₅) constructor have : 0 < min δ₄ δ₅ := by exact lt_min δ₄pos δ₅pos apply lt_min δ₀pos this intro x' h' have hp₀ : ‖x - x'‖ ≤ δ₀ := by have : min δ₀ (min δ₄ δ₅) ≤ δ₀ := by exact min_le_left δ₀ (min δ₄ δ₅) apply le_trans h' this have hp₁ : ‖x - x'‖ ≤ δ₄ := by have h₀ : min δ₀ (min δ₄ δ₅) ≤ (min δ₄ δ₅) := by exact min_le_right δ₀ (min δ₄ δ₅) have h₂ : min δ₄ δ₅ ≤ δ₄ := by exact min_le_left δ₄ δ₅ have h₃ : ‖x - x'‖ ≤ (min δ₄ δ₅) := by apply le_trans h' h₀ apply le_trans h₃ h₂ have hp₂ : ‖x - x'‖ ≤ δ₅ := by have h₀ : min δ₀ (min δ₄ δ₅) ≤ (min δ₄ δ₅) := by exact min_le_right δ₀ (min δ₄ δ₅) have h₂ : min δ₄ δ₅ ≤ δ₅ := by exact min_le_right δ₄ δ₅ have h₃ : ‖x - x'‖ ≤ (min δ₄ δ₅) := by apply le_trans h' h₀ apply le_trans h₃ h₂ have l0 : 0 < ‖f x'‖ := by have h' : ‖f x‖/2 ≤ ‖f x'‖ := hδ₀ x' hp₀ have h'' : 0 < ‖f x‖/2 := by apply div_pos apply Iff.mpr norm_pos_iff h₁ norm_num apply lt_of_lt_of_le h'' h' have l' : f x' ≠ 0 := by apply Iff.mp norm_pos_iff l0 have k₁ : 1 / f x' - 1 / f x = (f x - f x')/(f x' * f x) := by rw [← inv_eq_one_div, ← inv_eq_one_div] exact inv_sub_inv l' h₁ have k₂ : (f x - f x')/(f x' * f x) = (f x - f x') * f x /(f x' * f x * f x) := by apply Eq.symm (mul_div_mul_right (f x - f x') (f x' * f x) h₁) have k₃ : ⟪ (-(1 / f x ^ 2) • grad), (x' - x)⟫ = -⟪grad, (x' - x)⟫/((f x) * (f x)) := by have h' : 1 / f x ^ 2 = 1 / (f x * f x) := by rw [← inv_eq_one_div] have : (f x) ^ 2 = (f x) * (f x) := by rw [pow_two] rw [this, inv_eq_one_div] rw [h'] have l1 : ⟪(-(1 / (f x * f x)) • grad), (x' - x)⟫ = -(1 / (f x * f x)) * ⟪grad, (x' - x)⟫ := by rw [inner_smul_left] rfl rw [l1, neg_mul, mul_comm, mul_one_div, neg_div] have k₄ : ‖1 / f x' - 1 / f x - - (⟪grad, (x' - x)⟫)/((f x) * (f x))‖ = ‖1 / f x' - 1 / f x + (⟪grad, (x' - x)⟫)/((f x) * (f x))‖ := by congr ring_nf have k₅ : (⟪grad, (x' - x)⟫)/((f x) * (f x)) = f x' * (⟪grad, (x' - x)⟫)/((f x') * ((f x) * (f x))) := by apply Eq.symm (mul_div_mul_left (⟪grad, (x' - x)⟫) ((f x) * (f x)) l') have k₆ : (f x - f x') * f x /(f x' * f x * f x) + f x' * (⟪grad, (x' - x)⟫)/(f x' * f x * f x) = ((f x - f x') * f x + f x' * (⟪grad, (x' - x)⟫))/(f x' * f x * f x) := by apply div_add_div_same ((f x - f x') * f x) (f x' * (⟪grad, (x' - x)⟫)) (f x' * f x * f x) have k₇ : ((f x - f x') * f x + f x' * inner grad (x' - x)) / (f x' * f x * f x) = (f x * (f x - f x' + inner grad (x' - x)) + (f x' * inner grad (x' - x) - f x * inner grad (x' - x))) / (f x' * f x * f x) := by have h' : (f x - f x') * f x + f x' * inner grad (x' - x) = f x * (f x - f x' + inner grad (x' - x)) + (f x' * (inner grad (x' - x)) - f x * (inner grad (x' - x))) := by linarith rw [h'] have k₈ : (f x * (f x - f x' + inner grad (x' - x)) + (f x' * inner grad (x' - x) - f x * inner grad (x' - x))) / (f x * f x * f x') = f x * (f x - f x' + inner grad (x' - x))/ (f x * f x * f x') + (f x' * inner grad (x' - x) - f x * inner grad (x' - x))/ (f x * f x * f x') := by apply add_div ((f x) * (f x - f x' + inner grad (x' - x))) (f x' * inner grad (x' - x) - f x * inner grad (x' - x)) (f x * f x * f x') have k₉ : f x' * f x * f x = f x * f x * f x' := by linarith have p₁ : ‖1 / f x' - 1 / f x - (- (⟪grad, (x' - x)⟫))/((f x) * (f x))‖ ≤ ε * ‖x' - x‖ := by rw [k₄, k₁, k₂, k₅] have : f x' * (f x * f x) = f x' * f x * f x := by rw [← mul_assoc] rw [this] rw [k₆, k₇, k₉] calc ‖(f x * (f x - f x' + inner grad (x' - x)) + (f x' * inner grad (x' - x) - f x * inner grad (x' - x))) / (f x * f x * f x')‖ = ‖f x * (f x - f x' + inner grad (x' - x))/ (f x * f x * f x') + (f x' * inner grad (x' - x) - f x * inner grad (x' - x))/ (f x * f x * f x')‖ := by rw [k₈] _ ≤ ‖f x * (f x - f x' + inner grad (x' - x))/ (f x * f x * f x')‖ + ‖(f x' * inner grad (x' - x) - f x * inner grad (x' - x))/ (f x * f x * f x')‖ := by apply norm_add_le ((f x) * (f x - f x' + inner grad (x' - x))/ (f x * f x * f x')) ((f x' * inner grad (x' - x) - f x * inner grad (x' - x))/ (f x * f x * f x')) _ ≤ (ε/2) * ‖x' - x‖ + (ε/2) * ‖x' - x‖ := by exact add_le_add (hδ₅ x' hp₂) (hδ₄ x' hp₁) _ = ε * ‖x' - x‖ := by linarith have j₁ : ‖1 / f x' - 1 / f x - (- (⟪grad, (x' - x)⟫))/((f x) * (f x))‖ = ‖1 / f x' - 1 / f x - inner ((-(1 / f x ^ ↑2) • grad)) (x' - x)‖ := by congr; rw [k₃] rw [j₁] at p₁ have l1 : ‖x - x'‖ = ‖x' - x‖ := by exact norm_sub_rev x x' rw [l1] apply p₁