Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat: define logarithmic derivatives #12804

Closed
wants to merge 50 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
50 commits
Select commit Hold shift + click to select a range
c32039f
WIP logarithmic derivatives
CBirkbeck May 10, 2024
4842302
save
CBirkbeck May 24, 2024
aefad56
golf and move diff.prod lemma
CBirkbeck May 27, 2024
11625c0
some doc strings
CBirkbeck May 27, 2024
c3c87e6
Merge remote-tracking branch 'origin/master' into logarithmic_derivat…
CBirkbeck May 27, 2024
b3bee69
lintr fix
CBirkbeck May 27, 2024
6553f9a
mathlib file
CBirkbeck May 27, 2024
11caae8
add differenitableAt.product
CBirkbeck May 27, 2024
1e0f0b9
fix mathlib
CBirkbeck May 27, 2024
c4e9ec1
rev update
CBirkbeck May 28, 2024
0dd6291
Merge remote-tracking branch 'origin/master' into differentiableAt_pr…
CBirkbeck May 28, 2024
92424f0
fix error
CBirkbeck May 28, 2024
ce25b56
add diffOn version
CBirkbeck May 28, 2024
5e41144
deviv version
CBirkbeck May 28, 2024
f0daf6b
Update Mathlib/Analysis/Calculus/Deriv/Mul.lean
CBirkbeck May 28, 2024
c3829f5
Update Mathlib/Analysis/Calculus/Deriv/Mul.lean
CBirkbeck May 28, 2024
71d6720
Update Mathlib/Analysis/Calculus/Deriv/Mul.lean
CBirkbeck May 28, 2024
e10fa19
remove bigops
CBirkbeck May 28, 2024
01c9fec
Merge branch 'differentiableAt_product' of https://github.com/leanpro…
CBirkbeck May 28, 2024
2014a5e
fix
CBirkbeck May 28, 2024
f597de9
forgotten within version
CBirkbeck May 29, 2024
9d37c03
remove bad lemma
CBirkbeck May 29, 2024
cbc9d98
Merge remote-tracking branch 'origin/differentiableAt_product' into l…
CBirkbeck May 29, 2024
7698169
re add the lost file!
CBirkbeck May 29, 2024
b52c9d9
fix
CBirkbeck May 29, 2024
b63f294
lint fix
CBirkbeck May 29, 2024
a636c77
some examples
CBirkbeck May 29, 2024
a00c3fb
tiny
CBirkbeck May 29, 2024
ddf2c4e
slight generalisation
CBirkbeck May 29, 2024
5fdd30d
clog lemma
CBirkbeck May 29, 2024
ea5f80f
doc string
CBirkbeck May 29, 2024
c4e1cae
Merge remote-tracking branch 'origin/master' into logarithmic_derivat…
CBirkbeck May 29, 2024
b8b965d
rev fixes
CBirkbeck Jun 16, 2024
4dbd00a
save
CBirkbeck Jun 16, 2024
e2eee81
fix lintr
CBirkbeck Jun 16, 2024
f7969a2
rev updates
CBirkbeck Jul 16, 2024
6f1c533
Merge remote-tracking branch 'origin/master' into logarithmic_derivat…
CBirkbeck Jul 16, 2024
50db781
Update Mathlib/Analysis/NormedSpace/LogarithmicDerivatives.lean
CBirkbeck Jul 16, 2024
152faee
split files
CBirkbeck Jul 22, 2024
2e99a0f
fix name
CBirkbeck Jul 22, 2024
4be543b
fix
CBirkbeck Jul 22, 2024
c7ad95a
fix 2
CBirkbeck Jul 22, 2024
f8b9d8c
name update
CBirkbeck Jul 22, 2024
0eea8f0
Merge branch 'master' into logarithmic_derivatives
urkud Jul 26, 2024
c08855a
Golf, drop unneeded assumptions
urkud Jul 26, 2024
8d0166b
Merge branch 'master' into logarithmic_derivatives
urkud Jul 26, 2024
1fd8ffc
Fix
urkud Jul 26, 2024
9eb6182
rev updates
CBirkbeck Jul 29, 2024
993a85a
Merge branch 'master' into logarithmic_derivatives
urkud Jul 29, 2024
3d67567
Update Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean
urkud Jul 29, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
105 changes: 105 additions & 0 deletions Mathlib/Analysis/Calculus/LogDeriv.lean
Original file line number Diff line number Diff line change
@@ -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

13 changes: 13 additions & 0 deletions Mathlib/Analysis/Complex/LocallyUniformLimit.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
9 changes: 9 additions & 0 deletions Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
8 changes: 8 additions & 0 deletions Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
45 changes: 45 additions & 0 deletions Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down
19 changes: 18 additions & 1 deletion Mathlib/Data/Complex/Exponential.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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]

Expand All @@ -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]

Expand Down Expand Up @@ -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]
Expand Down
Loading