[Merged by Bors] - feat: define logarithmic derivatives

Mathlib.lean

@@ -970,6 +970,7 @@ import Mathlib.Analysis.Calculus.LocalExtr.Basic
 import Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
 import Mathlib.Analysis.Calculus.LocalExtr.Polynomial
 import Mathlib.Analysis.Calculus.LocalExtr.Rolle
+import Mathlib.Analysis.Calculus.LogDeriv
 import Mathlib.Analysis.Calculus.MeanValue
 import Mathlib.Analysis.Calculus.Monotone
 import Mathlib.Analysis.Calculus.ParametricIntegral

Mathlib/Analysis/Calculus/LogDeriv.lean

@@ -0,0 +1,105 @@
+/-
+Copyright (c) 2024 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+import Mathlib.Analysis.Calculus.Deriv.ZPow
+
+/-!
+# Logarithmic Derivatives
+
+We define the logarithmic derivative of a function f as `deriv f / f`. We then prove some basic
+facts about this, including how it changes under multiplication and composition.
+
+-/
+
+noncomputable section
+
+open Filter Function
+
+open scoped Topology BigOperators Classical
+
+variable {𝕜 𝕜': Type*} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜']
+  [NormedAlgebra 𝕜 𝕜']
+
+/-- The logarithmic derivative of a function defined as `deriv f /f`. Note that it will be zero
+at `x` if `f` is not DifferentiableAt `x`. -/
+def logDeriv (f : 𝕜 → 𝕜') :=
+  deriv f / f
+
+theorem logDeriv_apply (f : 𝕜 → 𝕜') (x : 𝕜) : logDeriv f x = deriv f x / f x := rfl
+
+lemma logDeriv_eq_zero_of_not_differentiableAt (f : 𝕜 → 𝕜') (x : 𝕜) (h : ¬DifferentiableAt 𝕜 f x) :
+    logDeriv f x = 0 := by
+  simp only [logDeriv_apply, deriv_zero_of_not_differentiableAt h, zero_div]
+
+@[simp]
+theorem logDeriv_id (x : 𝕜) : logDeriv id x = 1 / x := by
+  simp [logDeriv_apply]
+
+@[simp] theorem logDeriv_id' (x : 𝕜) : logDeriv (·) x = 1 / x := logDeriv_id x
+
+@[simp]
+theorem logDeriv_const (a : 𝕜') : logDeriv (fun _ : 𝕜 ↦ a) = 0 := by
+  ext
+  simp [logDeriv_apply]
+
+theorem logDeriv_mul {f g : 𝕜 → 𝕜'} (x : 𝕜) (hf : f x ≠ 0) (hg : g x ≠ 0)
+    (hdf : DifferentiableAt 𝕜 f x) (hdg : DifferentiableAt 𝕜 g x) :
+      logDeriv (fun z => f z * g z) x = logDeriv f x + logDeriv g x := by
+  simp only [logDeriv_apply, deriv_mul hdf hdg]
+  field_simp [mul_comm]
+
+theorem logDeriv_mul_const {f : 𝕜 → 𝕜'} (x : 𝕜) (a : 𝕜') (ha : a ≠ 0):
+    logDeriv (fun z => f z * a) x = logDeriv f x := by
+  simp only [logDeriv_apply, deriv_mul_const_field, mul_div_mul_right _ _ ha]
+
+theorem logDeriv_const_mul {f : 𝕜 → 𝕜'} (x : 𝕜) (a : 𝕜') (ha : a ≠ 0):
+    logDeriv (fun z => a * f z) x = logDeriv f x := by
+  simp only [logDeriv_apply, deriv_const_mul_field, mul_div_mul_left _ _ ha]
+
+/-- The logarithmic derivative of a finite product is the sum of the logarithmic derivatives. -/
+theorem logDeriv_prod {ι : Type*} (s : Finset ι) (f : ι → 𝕜 → 𝕜') (x : 𝕜) (hf : ∀ i ∈ s, f i x ≠ 0)
+    (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) :
+    logDeriv (∏ i ∈ s, f i ·) x = ∑ i ∈ s, logDeriv (f i) x := by
+  induction s using Finset.cons_induction with
+  | empty => simp
+  | cons a s ha ih =>
+    rw [Finset.forall_mem_cons] at hf hd
+    simp_rw [Finset.prod_cons, Finset.sum_cons]
+    rw [logDeriv_mul, ih hf.2 hd.2]
+    · exact hf.1
+    · simpa [Finset.prod_eq_zero_iff] using hf.2
+    · exact hd.1
+    · exact .finset_prod hd.2
+
+lemma logDeriv_fun_zpow {f : 𝕜 → 𝕜'} {x : 𝕜} (hdf : DifferentiableAt 𝕜 f x) (n : ℤ) :
+    logDeriv (f · ^ n) x = n * logDeriv f x := by
+  rcases eq_or_ne n 0 with rfl | hn; · simp
+  rcases eq_or_ne (f x) 0 with hf | hf
+  · simp [logDeriv_apply, zero_zpow, *]
+  · rw [logDeriv_apply, ← comp_def (·^n), deriv.comp _ (differentiableAt_zpow.2 <| .inl hf) hdf,
+      deriv_zpow, logDeriv_apply]
+    field_simp [zpow_ne_zero, zpow_sub_one₀ hf]
+    ring
+
+lemma logDeriv_fun_pow {f : 𝕜 → 𝕜'} {x : 𝕜} (hdf : DifferentiableAt 𝕜 f x) (n : ℕ) :
+    logDeriv (f · ^ n) x = n * logDeriv f x :=
+  mod_cast logDeriv_fun_zpow hdf n
+
+@[simp]
+lemma logDeriv_zpow (x : 𝕜) (n : ℤ) : logDeriv (· ^ n) x = n / x := by
+  rw [logDeriv_fun_zpow (by fun_prop), logDeriv_id', mul_one_div]
+
+@[simp]
+lemma logDeriv_pow (x : 𝕜) (n : ℕ) : logDeriv (· ^ n) x = n / x :=
+  mod_cast logDeriv_zpow x n
+
+@[simp] lemma logDeriv_inv (x : 𝕜) : logDeriv (·⁻¹) x = -1 / x := by
+  simpa using logDeriv_zpow x (-1)
+
+theorem logDeriv_comp {f : 𝕜' → 𝕜'} {g : 𝕜 → 𝕜'} {x : 𝕜} (hf : DifferentiableAt 𝕜' f (g x))
+    (hg : DifferentiableAt 𝕜 g x) : logDeriv (f ∘ g) x = logDeriv f (g x) * deriv g x := by
+  simp only [logDeriv, Pi.div_apply, deriv.comp _ hf hg, comp_apply]
+  ring
+

Mathlib/Analysis/Complex/LocallyUniformLimit.lean

@@ -187,4 +187,17 @@ theorem hasSum_deriv_of_summable_norm {u : ι → ℝ} (hu : Summable u)
 
 end Tsums
 
+section LogDeriv
+
+/-- The logarithmic derivative of a sequence of functions converging locally uniformly to a
+function is the logarithmic derivative of the limit function. -/
+theorem logDeriv_tendsto {ι : Type*} {p : Filter ι} (f : ι → ℂ → ℂ) (g : ℂ → ℂ)
+    {s : Set ℂ} (hs : IsOpen s) (x : s) (hF : TendstoLocallyUniformlyOn f g p s)
+    (hf : ∀ᶠ n : ι in p, DifferentiableOn ℂ (f n) s) (hg : g x ≠ 0) :
+    Tendsto (fun n : ι => logDeriv (f n) x) p (𝓝 ((logDeriv g) x)) := by
+  simp_rw [logDeriv]
+  apply Tendsto.div ((hF.deriv hf hs).tendsto_at x.2) (hF.tendsto_at x.2) hg
+
+end LogDeriv
+
 end Complex

Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson
 -/
 import Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
+import Mathlib.Analysis.Calculus.LogDeriv
 import Mathlib.Analysis.SpecialFunctions.Complex.Log
 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
 
@@ -133,4 +134,12 @@ theorem Differentiable.clog {f : E → ℂ} (h₁ : Differentiable ℂ f)
     (h₂ : ∀ x, f x ∈ slitPlane) : Differentiable ℂ fun t => log (f t) := fun x =>
   (h₁ x).clog (h₂ x)
 
+/-- The derivative of `log ∘ f` is the logarithmic derivative provided `f` is differentiable and
+we are on the slitPlane. -/
+lemma Complex.deriv_log_comp_eq_logDeriv {f : ℂ → ℂ} {x : ℂ} (h₁ : DifferentiableAt ℂ f x)
+    (h₂ : f x ∈ Complex.slitPlane) : deriv (Complex.log ∘ f) x = logDeriv f x := by
+  have A := (HasDerivAt.clog h₁.hasDerivAt h₂).deriv
+  rw [← h₁.hasDerivAt.deriv] at A
+  simp only [logDeriv, Pi.div_apply, ← A, Function.comp_def]
+
 end LogDeriv

Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne
 -/
 import Mathlib.Analysis.Calculus.Deriv.Pow
+import Mathlib.Analysis.Calculus.LogDeriv
 import Mathlib.Analysis.SpecialFunctions.Log.Basic
 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
 import Mathlib.Tactic.AdaptationNote
@@ -109,6 +110,13 @@ theorem deriv.log (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) :
     deriv (fun x => log (f x)) x = deriv f x / f x :=
   (hf.hasDerivAt.log hx).deriv
 
+/-- The derivative of `log ∘ f` is the logarithmic derivative provided `f` is differentiable and
+`f x  ≠ 0`. -/
+lemma Real.deriv_log_comp_eq_logDeriv {f : ℝ → ℝ} {x : ℝ} (h₁ : DifferentiableAt ℝ f x)
+    (h₂ : f x ≠ 0) : deriv (log ∘ f) x = logDeriv f x := by
+  simp only [ne_eq, logDeriv, Pi.div_apply, ← deriv.log h₁ h₂]
+  rfl
+
 end deriv
 
 section fderiv

Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson
 -/
 import Mathlib.Order.Monotone.Odd
+import Mathlib.Analysis.Calculus.LogDeriv
 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 
@@ -968,6 +969,50 @@ theorem ContDiffWithinAt.sinh {n} (hf : ContDiffWithinAt ℝ n f s x) :
     ContDiffWithinAt ℝ n (fun x => Real.sinh (f x)) s x :=
   Real.contDiff_sinh.contDiffAt.comp_contDiffWithinAt x hf
 
+section LogDeriv
+
+@[simp]
+theorem Complex.logDeriv_sin : logDeriv (Complex.sin) = Complex.cot := by
+  ext
+  rw [logDeriv, Complex.deriv_sin, Pi.div_apply, Complex.cot]
+
+@[simp]
+theorem Real.logDeriv_sin : logDeriv (Real.sin) = Real.cot := by
+  ext
+  rw [logDeriv, Real.deriv_sin, Pi.div_apply, Real.cot_eq_cos_div_sin]
+
+@[simp]
+theorem Complex.logDeriv_cos : logDeriv (Complex.cos) = -Complex.tan := by
+  ext
+  rw [logDeriv, Complex.deriv_cos', Pi.div_apply, Pi.neg_apply, Complex.tan, neg_div]
+
+@[simp]
+theorem Real.logDeriv_cos : logDeriv (Real.cos) = -Real.tan := by
+  ext
+  rw [logDeriv, Real.deriv_cos', Pi.div_apply, Pi.neg_apply, neg_div, Real.tan_eq_sin_div_cos ]
+
+@[simp]
+theorem Complex.logDeriv_cosh : logDeriv (Complex.cosh) = Complex.tanh := by
+  ext
+  rw [logDeriv, Complex.deriv_cosh, Pi.div_apply, Complex.tanh]
+
+@[simp]
+theorem Real.logDeriv_cosh : logDeriv (Real.cosh) = Real.tanh := by
+  ext
+  rw [logDeriv, Real.deriv_cosh, Pi.div_apply, Real.tanh_eq_sinh_div_cosh]
+
+@[simp]
+theorem Complex.LogDeriv_exp : logDeriv (Complex.exp) = 1 := by
+  ext
+  rw [logDeriv, Complex.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
+
+@[simp]
+theorem Real.LogDeriv_exp : logDeriv (Real.exp) = 1 := by
+  ext
+  rw [logDeriv, Real.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
+
+end LogDeriv
+
 end
 
 namespace Mathlib.Meta.Positivity

Mathlib/Data/Complex/Exponential.lean

@@ -552,6 +552,9 @@ theorem tan_zero : tan 0 = 0 := by simp [tan]
 theorem tan_eq_sin_div_cos : tan x = sin x / cos x :=
   rfl
 
+theorem cot_eq_cos_div_sin : cot x = cos x / sin x :=
+  rfl
+
 theorem tan_mul_cos {x : ℂ} (hx : cos x ≠ 0) : tan x * cos x = sin x := by
   rw [tan_eq_sin_div_cos, div_mul_cancel₀ _ hx]
 
@@ -560,14 +563,24 @@ theorem tan_neg : tan (-x) = -tan x := by simp [tan, neg_div]
 
 theorem tan_conj : tan (conj x) = conj (tan x) := by rw [tan, sin_conj, cos_conj, ← map_div₀, tan]
 
+theorem cot_conj : cot (conj x) = conj (cot x) := by rw [cot, sin_conj, cos_conj, ← map_div₀, cot]
+
 @[simp]
 theorem ofReal_tan_ofReal_re (x : ℝ) : ((tan x).re : ℂ) = tan x :=
   conj_eq_iff_re.1 <| by rw [← tan_conj, conj_ofReal]
 
+@[simp]
+theorem ofReal_cot_ofReal_re (x : ℝ) : ((cot x).re : ℂ) = cot x :=
+  conj_eq_iff_re.1 <| by rw [← cot_conj, conj_ofReal]
+
 @[simp, norm_cast]
 theorem ofReal_tan (x : ℝ) : (Real.tan x : ℂ) = tan x :=
   ofReal_tan_ofReal_re _
 
+@[simp, norm_cast]
+theorem ofReal_cot (x : ℝ) : (Real.cot x : ℂ) = cot x :=
+  ofReal_cot_ofReal_re _
+
 @[simp]
 theorem tan_ofReal_im (x : ℝ) : (tan x).im = 0 := by rw [← ofReal_tan_ofReal_re, ofReal_im]
 
@@ -744,7 +757,11 @@ nonrec theorem cos_add_cos : cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y
   ofReal_injective <| by simp [cos_add_cos]
 
 nonrec theorem tan_eq_sin_div_cos : tan x = sin x / cos x :=
-  ofReal_injective <| by simp [tan_eq_sin_div_cos]
+  ofReal_injective <| by simp only [ofReal_tan, tan_eq_sin_div_cos, ofReal_div, ofReal_sin,
+    ofReal_cos]
+
+nonrec theorem cot_eq_cos_div_sin : cot x = cos x / sin x :=
+  ofReal_injective <| by simp [cot_eq_cos_div_sin]
 
 theorem tan_mul_cos {x : ℝ} (hx : cos x ≠ 0) : tan x * cos x = sin x := by
   rw [tan_eq_sin_div_cos, div_mul_cancel₀ _ hx]