From 6ea738c862a8df1a5353c6476808ffcd96b4fb10 Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Mon, 29 Jul 2024 17:43:42 +0000 Subject: [PATCH] feat: define logarithmic derivatives (#12804) We define the logarithmic derivative of a function as `f'/f` and then prove some basic facts about this. Specifially some things that will be needed for the Mittag-Leffler Expansion for Cotangent Function. Co-authored-by: Chris Birkbeck Co-authored-by: Yury G. Kudryashov --- Mathlib.lean | 1 + Mathlib/Analysis/Calculus/LogDeriv.lean | 105 ++++++++++++++++++ .../Analysis/Complex/LocallyUniformLimit.lean | 13 +++ .../SpecialFunctions/Complex/LogDeriv.lean | 9 ++ .../Analysis/SpecialFunctions/Log/Deriv.lean | 8 ++ .../SpecialFunctions/Trigonometric/Deriv.lean | 45 ++++++++ Mathlib/Data/Complex/Exponential.lean | 19 +++- 7 files changed, 199 insertions(+), 1 deletion(-) create mode 100644 Mathlib/Analysis/Calculus/LogDeriv.lean diff --git a/Mathlib.lean b/Mathlib.lean index 152ef3b82f9d6e..85b9a14286dd3c 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Analysis/Calculus/LogDeriv.lean b/Mathlib/Analysis/Calculus/LogDeriv.lean new file mode 100644 index 00000000000000..525cbcab01852a --- /dev/null +++ b/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 + diff --git a/Mathlib/Analysis/Complex/LocallyUniformLimit.lean b/Mathlib/Analysis/Complex/LocallyUniformLimit.lean index 144330a5f95de4..8151998153a2a7 100644 --- a/Mathlib/Analysis/Complex/LocallyUniformLimit.lean +++ b/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 diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean b/Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean index 7c6c607af0deca..f92d4934e22ece 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean +++ b/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 diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean index 5f728343239c1c..4e974d98df1d6d 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean +++ b/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 diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean index 9f56767e8c8155..9293d0b7de6f3d 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean +++ b/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 diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean index a703f1c004be8a..2f84e4fb047137 100644 --- a/Mathlib/Data/Complex/Exponential.lean +++ b/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]