Power series / bound for complex logarithm

Stream: Is there code for X?

[Michael Stoll]

There is docs#Real.abs_log_sub_add_sum_range_le , but I can't find an analogue for the complex logarithm.
What I really need is something like

example {x : ℂ} (hx : ‖x‖ < 1) : ‖Complex.log (1 - x)⁻¹ - x‖ ≤ ‖x‖ ^ 2 / (1 - ‖x‖)

(which follows by a fairly rough estimate of the power series, but the power series expansion seems to be missing as well -- there are statements like docs#expSeries_div_hasSum_exp on the exponential series, but nothing mentioning "logSeries".)

Wasn't there some activity on holo-/meromorphic functions and power series at some point?

[Michael Stoll]

I think one possible way to get something like this is to use
(*) $\displaystyle \log(1 + z) = \int_0^1 \frac{z}{1+tz}\,dt$,
then
$\displaystyle |\log(1+z) - z| = \left|\int_0^1 \frac{-tz^2}{1+tz}\,dt\right| \le \frac{|z|^2}{1-|z|} \int_0^1 t\,dt = \frac{|z|^2}{2(1-|z|)}$.

What would be the idiomatic way to obtain (*)? I think I can take it from there.

[Floris van Doorn]

docs#integral_inv_of_pos together with docs#MeasureTheory.integral_add_left_eq_self docs#intervalIntegral.integral_comp_add_left should get you most of the way

[Michael Stoll]

docs#integral_inv_of_pos is for the real logarithm. but I need it for the complex one.

[Michael Stoll]

Albeit for a real (but complex-valued) path integral...

[Floris van Doorn]

Then I'm not sure. Maybe it's instructive to look how docs#integral_exp_mul_complex is derived from docs#integral_exp

[Michael Stoll]

There is Complex_differentiableAt_xxx, for xxx in cos, cosh, exp, Gamma, sin, sinh, tan, but not log!
Why did the complex logarithm receive so little love?

[Kevin Buzzard]

because it's multi-valued?

[Michael Stoll]

It is still differentiable outside the negative real axis.

[Michael Stoll]

(The principal branch, which is how Complex.log is defined.)

[Michael Stoll]

Also, its multi-valuedness is what makes it more interesting!

[Ruben Van de Velde]

Possibly because nobody's used it much so far

[Michael Stoll]

I would have thought that log would be included as soon as somebody does special functions...

[Michael Stoll]

Now I am having the problem that docs#intervalIntegral.integral_deriv_eq_sub' requires deriv f = f' for f a function on all of the reals, where it should suffice to have it on the relevant interval. (My f is t ↦ log (1 + t * z), and of course I would like to use the chain rule. I think that even assuming

lemma Complex.hasDerivAt_log {z : ℂ} (h₀ : z ≠ 0) (h : z.arg ≠ -Real.pi) :
    HasDerivAt log (1 / z) z

I cannot get to deriv log <something> easily, since the <something> would have to be zero along the negative real axis.)

Ideas?

[Michael Stoll]

I would think that it would be sufficient to assume HasDerivAt f (f' x) x for all x in Set.uIcc a b in docs#intervalIntegral.integral_deriv_eq_sub'.

[Michael Stoll]

Also, why use uIcc instead of Icc for real intervals?

[Ruben Van de Velde]

Does docs#integral_eq_sub_of_hasDerivAt help?

[Michael Stoll]

docs#intervalIntegral.integral_eq_sub_of_hasDerivAt ? Possibly; I'll have a look.

[Michael Stoll]

OK, I've made some progress.

Now, in order to prove that the complex log has the correct derivative, I would like to use the characterization of complex differentiability in terms of real derivatives (Cauxhy-Riemann equations). However, I can't find anything resembling that in Mathlib. I'd appreciate any pointers!

[Kevin Buzzard]

ha ha Cauchy-Riemann is just the sort of thing that I can imagine that we don't have, because the partial derivative people don't like to choose coordinates :-)

[Heather Macbeth]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Complex/RealDeriv.html

[Heather Macbeth]

`DifferentiableAt.conformalAt` states that a real-differentiable function with a nonvanishing
differential from the complex plane into an arbitrary complex-normed space is conformal at a point
if it's holomorphic at that point. This is a version of Cauchy-Riemann equations.

## TODO

* The classical form of Cauchy-Riemann equations

[Michael Stoll]

Could somebody please do it? :pray:

[Michael Stoll]

or prove

lemma Complex.hasDerivAt_log {z : ℂ} (h₀ : z ≠ 0) (h : z.arg ≠ Real.pi) :
    HasDerivAt log (1 / z) z := sorry

[Heather Macbeth]

Sorry, I'm confused, is docs#Complex.hasStrictDerivAt_log no good?

[Michael Stoll]

It seems to be hard to find, compared with docs#Complex.hasDerivAt_exp and friends.

[Michael Stoll]

At least, I think I tried fairly hard and did not find it...

[Heather Macbeth]

This is probably a useful form for getting the real derivative (as a matrix): docs#HasStrictDerivAt.complexToReal_fderiv

[Michael Stoll]

There is no docs#Complex.hasDerivAt_log . Why not?

[Heather Macbeth]

Likely just laziness on the part of the person who added the StrictDeriv version, it would be a welcome (1-line) pr.

[Michael Stoll]

example (a b : ℂ) : ‖a‖ - ‖b‖ ≤ ‖a + b‖

is not found by exact?. There is docs#norm_sub_norm_le , but apparently no version with a sum on the right.

[Ruben Van de Velde]

Also docs#norm_le_add_norm_add is close, but this seems worth adding as well!

[Michael Stoll]

:bed:

[Michael Stoll]

I have the following.

import Mathlib

namespace Complex

lemma xxx {f f' : ℂ → ℂ} {z₀ z₁ : ℂ}
    (hcont : ContinuousOn (fun t : ℝ ↦ f' (z₀ + t * z₁)) (Set.Icc 0 1))
    (hderiv : ∀ t ∈ Set.Icc (0 : ℝ) 1, HasDerivAt f (f' (z₀ + t * z₁)) (z₀ + t * z₁)) :
    f (z₀ + z₁) = f z₀ + z₁ * ∫ t in (0 : ℝ)..1, f' (z₀ + t * z₁) := ...

I assume this would be a reasonable addition to Mathlib (in particular since I'm using it to prove further results).
What would be a good name for this lemma? @Heather Macbeth

[Heather Macbeth]

Let's be mathlib-y -- can you generalize the domain to IsROrC and the codomain to a normed space over that field?

[Michael Stoll]

I can try, but not tonight.

[Heather Macbeth]

I think it would make sense to have a similar name to the names for FTC-2, like docs#intervalIntegral.integral_eq_sub_of_hasDerivAt. This version uses MeasureTheory.integral, not intervalIntegral, so maybe it should be called something like MeasureTheory.integral_eq_sub_of_hasDerivAt ... that is still not a perfect name since it doesn't exactly match the form of theorem you have, but it can be a place to get started.

[Michael Stoll]

I'm trying to prove invariance of derivatives under shift of the argument

lemma _HasDerivAt.comp_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] (a x : 𝕜) {𝕜' : Type u_1}
    [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h' : 𝕜'}
    (hh : HasDerivAt h h' (a + x)) :
    HasDerivAt (fun x ↦ h (a + x)) h' x  := ...

but I'm stuck since apparently neither HasDerivAt.comp nor HasDerivAt.scomp seem to apply. The first one requires the outer function to be of type 𝕜' → 𝕜', and when I try to use the second, I run into type class problems.
(BTW, apply? has proven to be decidedly unhelpful with goals involving HasDerivAt. It basically never suggests lemmas like HasDerivAt.add etc.)

I need it only in the case when 𝕜 = 𝕜' = ℂ (then HasDerivAt.comp works), but I'm surprised that the statement above is not in Mathib (unless I have missed something).

[Ruben Van de Velde]

Does this help?

import Mathlib
lemma _HasDerivAt.comp_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] (a x : 𝕜) {𝕜' : Type u_1}
    [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h' : 𝕜'}
    (hh : HasDerivAt h h' (a + x)) :
    HasDerivAt (fun x ↦ h (a + x)) h' x  := by
  have : HasDerivAt (fun x ↦ (a + x)) _ x := hasDerivAt_id' x |>.const_add a
  have := HasDerivAt.scomp  (𝕜 := 𝕜) x hh this
  simpa [Function.comp_def] using this

[Michael Stoll]

I notice that you use a "forward reasoning" approach here, which is what I was ending up doing in similar situations.

import Mathlib

example {f g : ℝ → ℂ} {x : ℝ} {a b : ℂ} (hf : HasDerivAt f a x) (hg : HasDerivAt g b x) :
    HasDerivAt (f + g) (a + b) x := by
  apply?
  sorry

suggests

Try this: refine hasDerivAt_iff_hasFDerivAt.mpr ?a✝
Try this: refine HasStrictDerivAt.hasDerivAt ?h
Try this: refine hasDerivWithinAt_univ.mp ?a✝
Try this: refine hasDerivAt_iff_tendsto.mpr ?a✝
Try this: refine hasDerivAt_iff_isLittleO.mpr ?a✝
Try this: refine hasDerivAt_iff_tendsto_slope_zero.mpr ?a✝
Try this: refine hasDerivAt_iff_tendsto_slope.mpr ?a✝
Try this: refine hasDerivAt_iff_isLittleO_nhds_zero.mpr ?a✝
Try this: refine hasDerivAt_of_hasDerivAt_of_ne ?f_diff ?hf ?hg
Try this: refine (Filter.EventuallyEq.hasDerivAt_iff ?h).mpr ?a✝
Try this: refine HasDerivAt.congr_of_eventuallyEq ?h ?h₁
Try this: refine (Filter.EventuallyEq.hasDerivAt_iff ?h).mp ?a✝
Try this: refine HasDerivWithinAt.hasDerivAt ?h ?hs
Try this: refine hasDerivAt_of_hasDerivAt_of_ne' ?f_diff ?hf ?hg x
Try this: refine hasDerivAt_of_tendstoUniformly ?hf' ?hf ?hfg x
Try this: refine hasDerivAt_of_tendstoUniformlyOnFilter ?hf' ?hf ?hfg
Try this: refine hasDerivAt_of_tendsto_locally_uniformly_on' ?hs ?hf' ?hf ?hfg ?hx
Try this: refine hasDerivAt_of_tendstoUniformlyOn ?hs ?hf' ?hf ?hfg x ?a✝
Try this: refine hasDerivAt_of_tendstoLocallyUniformlyOn ?hs ?hf' ?hf ?hfg ?hx

but misses the "obvious" suggestion HasDerivAt.add (and exact? "could not close the goal," which can be done by exact HasDerivAt.add hf hg).
Replacing apply? above by refine HasDerivAt.add ?_ ?_ works here, so I'm a bit at a loss why this is.
@Scott Morrison

In more involved use cases, the refine HasDerivAt.... ?_ ?_ tends to get stuck in typeclass search, which I assume makes it hard to provide automation for this kind of situation.

[Ruben Van de Velde]

I think I saw it mentioned somewhere that the lambdas in the conclusion of theorems like that make it hard on apply?

[Scott Morrison]

No, it's something more basic than that.

set_option trace.Tactic.librarySearch.lemmas true

causes exact? / apply? to show that lemmas that it will consider, before it tries applying any. HasDerivAt.add isn't in this list, but I don't understand why yet.

[Scott Morrison]

Oh, no @Ruben Van de Velde is correct.

[Scott Morrison]

example {f g : ℝ → ℂ} {x : ℝ} {a b : ℂ} (hf : HasDerivAt f a x) (hg : HasDerivAt g b x) :
    HasDerivAt (fun x => f x + g x) (a + b) x := by
  exact?

works fine.

[Scott Morrison]

@Jovan Gerbscheid, does your replacement for DiscrTree cope with this situation?

[Scott Morrison]

If so, what do we need to do to get it into Std?

[Scott Morrison]

I'm not sure why

theorem HasDerivAt.add (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) :
    HasDerivAt (fun x => f x + g x) (f' + g') x := ...

is written like that in the first place, instead of just

theorem HasDerivAt.add (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) :
    HasDerivAt (f + g) (f' + g') x := ...

Mathlib seems to compile happily, and this would make exact? work here.

[Scott Morrison]

@Sebastien Gouezel, @Yury G. Kudryashov, could I summon one of you to see if you have an idea about this last question?

[Scott Morrison]

Okay, I have convinced myself that we can't really change this lemmas. Sorry for the noise.

[Scott Morrison]

Either rw won't work in the presence of a fun in the goal, or convert gives bad goals.

[Scott Morrison]

(The HasDerivAt.add above does seem to be able to be changed, but its relatives about sub and so and cause problems.)

[Scott Morrison]

One can see the problem with the current DiscrTree implementation via:

import Mathlib

#check HasDerivAt.add
#check HasDerivAt

open Lean Elab Meta

deriving instance Repr for Mathlib.Tactic.LibrarySearch.DeclMod

#eval show MetaM _ from do
  let n := ``HasDerivAt.add
  Mathlib.Tactic.LibrarySearch.processLemma n (← getConstInfo n)

which prints:

#[(#[Lean.Meta.DiscrTree.Key.const `HasDerivAt 8, Lean.Meta.DiscrTree.Key.star, Lean.Meta.DiscrTree.Key.star,
     Lean.Meta.DiscrTree.Key.star, Lean.Meta.DiscrTree.Key.star, Lean.Meta.DiscrTree.Key.star,
     Lean.Meta.DiscrTree.Key.other, Lean.Meta.DiscrTree.Key.const `HAdd.hAdd 6, Lean.Meta.DiscrTree.Key.star,
     Lean.Meta.DiscrTree.Key.star, Lean.Meta.DiscrTree.Key.star, Lean.Meta.DiscrTree.Key.star,
     Lean.Meta.DiscrTree.Key.star, Lean.Meta.DiscrTree.Key.star, Lean.Meta.DiscrTree.Key.star],
   `HasDerivAt.add,
   Mathlib.Tactic.LibrarySearch.DeclMod.none)]

The .other key for the lambda is the problem here: it then refuses to match f + g.

As a hack, I could replace these .other keys with .star when building the DiscrTree for exact?...

Hoping that @Jovan Gerbscheid has good news otherwise. :-)

[Yaël Dillies]

convert worked fine with such lemmas in Lean 3. I believe it's just less brave in Lean 4 (for performance reasons).

[Jovan Gerbscheid]

My version of DiscrTree would encode HasDerivAt as follows:
[⟨HasDerivAt, 8⟩, *0, *1, *2, *3, *4, λ, ⟨HAdd.hAdd, 6⟩, *2, *2, *2, *5, *6, *7, ⟨HAdd.hAdd, 6⟩, *2, *2, *2, *8, *9, *10, *11]

[Jovan Gerbscheid]

So yes, it indexes the lambda and the + inside.

[Jovan Gerbscheid]

Michael Stoll said:

I notice that you use a "forward reasoning" approach here, which is what I was ending up doing in similar situations.

import Mathlib

example {f g : ℝ → ℂ} {x : ℝ} {a b : ℂ} (hf : HasDerivAt f a x) (hg : HasDerivAt g b x) :
    HasDerivAt (f + g) (a + b) x := by
  apply?
  sorry

suggests

Try this: refine hasDerivAt_iff_hasFDerivAt.mpr ?a✝
Try this: refine HasStrictDerivAt.hasDerivAt ?h
Try this: refine hasDerivWithinAt_univ.mp ?a✝
Try this: refine hasDerivAt_iff_tendsto.mpr ?a✝
Try this: refine hasDerivAt_iff_isLittleO.mpr ?a✝
Try this: refine hasDerivAt_iff_tendsto_slope_zero.mpr ?a✝
Try this: refine hasDerivAt_iff_tendsto_slope.mpr ?a✝
Try this: refine hasDerivAt_iff_isLittleO_nhds_zero.mpr ?a✝
Try this: refine hasDerivAt_of_hasDerivAt_of_ne ?f_diff ?hf ?hg
Try this: refine (Filter.EventuallyEq.hasDerivAt_iff ?h).mpr ?a✝
Try this: refine HasDerivAt.congr_of_eventuallyEq ?h ?h₁
Try this: refine (Filter.EventuallyEq.hasDerivAt_iff ?h).mp ?a✝
Try this: refine HasDerivWithinAt.hasDerivAt ?h ?hs
Try this: refine hasDerivAt_of_hasDerivAt_of_ne' ?f_diff ?hf ?hg x
Try this: refine hasDerivAt_of_tendstoUniformly ?hf' ?hf ?hfg x
Try this: refine hasDerivAt_of_tendstoUniformlyOnFilter ?hf' ?hf ?hfg
Try this: refine hasDerivAt_of_tendsto_locally_uniformly_on' ?hs ?hf' ?hf ?hfg ?hx
Try this: refine hasDerivAt_of_tendstoUniformlyOn ?hs ?hf' ?hf ?hfg x ?a✝
Try this: refine hasDerivAt_of_tendstoLocallyUniformlyOn ?hs ?hf' ?hf ?hfg ?hx

but misses the "obvious" suggestion HasDerivAt.add (and exact? "could not close the goal," which can be done by exact HasDerivAt.add hf hg).
Replacing apply? above by refine HasDerivAt.add ?_ ?_ works here, so I'm a bit at a loss why this is.
Scott Morrison

In more involved use cases, the refine HasDerivAt.... ?_ ?_ tends to get stuck in typeclass search, which I assume makes it hard to provide automation for this kind of situation.

The problem here is that there are two equivalent ways of adding two functions: f + g or fun x => f x + g x. The lemma you want to find uses fun x => f x + g x, and since the addition in f + g is not reducible, no version of DiscrTree will match up these expressions.

[Jovan Gerbscheid]

This makes me wonder whether it would be a good idea for DiscrTree to attempt unfolding expressions further, and matching the unfolded expression. (In this case unfolding f + g)

[Jovan Gerbscheid]

Is there a particular reason why hasDerivAt.add uses fun x => f x + g x instead of f + g?

[Ruben Van de Velde]

Have you read Scott's messages earlier in this thread starting with "Okay, I have convinced myself"?

[Jovan Gerbscheid]

Oh sorry, I hadn't. But I don't quite get it. This works fine for me:

example (p : (Nat → Int) → Prop) (h : ∀ {f g}, p (f + g)) : p (fun x => x + 1) := by
  convert h

[Jovan Gerbscheid]

looking at the code for Lean.MVarId.congrCore!, it loops through this list:

def Lean.MVarId.congrPasses! :
    List (String × (Congr!.Config → MVarId → MetaM (Option (List MVarId)))) :=
  [("user congr", userCongr?),
   ("hcongr lemma", smartHCongr?),
   ("congr simp lemma", congrSimp?),
   ("Subsingleton.helim", fun _ => subsingletonHelim?),
   ("obvious funext", fun _ => obviousFunext?),
   ("obvious hfunext", fun _ => obviousHfunext?),
   ("congr_implies", fun _ => congrImplies?'),
   ("congr_pi", fun _ => congrPi?)]

And "obvious funext" seems to do the thing we want: matching f + g with a lambda using funext. (so the behaviour is expected)

[Jovan Gerbscheid]

So I don't see a problem with using f + g in the library lemma.

[Patrick Massot]

Requiring convertis a problem.

[Michael Stoll]

Heather Macbeth said:

Let's be mathlib-y -- can you generalize the domain to IsROrC and the codomain to a normed space over that field?

@Heather Macbeth It seems I need to add

noncomputable instance {C E : Type*} [IsROrC C] [NormedAddCommGroup E] [NormedSpace C E] :
    NormedSpace ℝ E := NormedSpace.restrictScalars ℝ C E

to get the statement to type-check. The next problem is that I use HasDerivAt.comp_ofReal in the proof, which does not work with C : IsROrC in place of ℂ. The proof of this involves Complex.ofRealClm.hasDerivAt whose counterpart IsROrC.ofRealClm.hasDerivAt gives an error

application type mismatch
  ContinuousLinearMap.hasDerivAt IsROrC.ofRealClm
argument
  IsROrC.ofRealClm
has type
  @ContinuousLinearMap ℝ ℝ Real.semiring Real.semiring (RingHom.id ℝ) ℝ UniformSpace.toTopologicalSpace
    Real.instAddCommMonoidReal ?m.478
    (@UniformSpace.toTopologicalSpace ?m.478
      (@PseudoMetricSpace.toUniformSpace ?m.478 SeminormedRing.toPseudoMetricSpace))
    NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule
    (@NormedSpace.toModule ℝ ?m.478 Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup
      NormedAlgebra.toNormedSpace') : Type ?u.467
but is expected to have type
  @ContinuousLinearMap ℝ ℝ DivisionSemiring.toSemiring DivisionSemiring.toSemiring (RingHom.id ℝ) ℝ
    UniformSpace.toTopologicalSpace NonUnitalNonAssocSemiring.toAddCommMonoid ?m.478
    (@UniformSpace.toTopologicalSpace ?m.478
      (@PseudoMetricSpace.toUniformSpace ?m.478 SeminormedAddCommGroup.toPseudoMetricSpace))
    AddCommGroup.toAddCommMonoid NormedSpace.toModule
    (@NormedSpace.toModule ℝ ?m.478 NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup
      ?m.480) : Type ?u.467

Maybe someone can provide an analogue of HasDerivAt.comp_ofReal that works in the ROrC situation?

[Michael Stoll]

The instance is actually bad, since it conflicts with NormedAlgebra.toNormedSpace' when E = C.
My statement is now

lemma xyz {C E : Type*} [IsROrC C] [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace C E]
    {f f' : C → E} {z₀ z₁ : C}
    (hcont : ContinuousOn (fun t : ℝ ↦ f' (z₀ + t * z₁)) (Set.Icc 0 1))
    (hderiv : ∀ t ∈ Set.Icc (0 : ℝ) 1, HasDerivAt f (f' (z₀ + t * z₁)) (z₀ + t * z₁)) :
    haveI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ C E
    f (z₀ + z₁) = f z₀ + z₁ • ∫ t in (0 : ℝ)..1, f' (z₀ + t * z₁) := ...

which is perhaps not so nice. Is there a better way?

[Michael Stoll]

I'm also having the problem that HasDerivAt.comp does not work as it did previously (for ℝ → ℂ → ℂ) in the situation ℝ → C → E. My derivative is of the form z₁ • f' (z₀ + ↑t * z₁), but for HasDerivAt.comp it has to be f' (z₀ + ↑t * z₁) * z₁. I'm giving up for today.

[Michael Stoll]

It seems that the better version is

lemma xyz {C E : Type*} [NontriviallyNormedField C] [NormedAlgebra ℝ C]
    [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace C E] [CompleteSpace E]
    [IsScalarTower ℝ C E] {f f' : C → E} {z₀ z₁ : C}
    (hcont : ContinuousOn (fun t : ℝ ↦ f' (z₀ + t • z₁)) (Set.Icc 0 1))
    (hderiv : ∀ t ∈ Set.Icc (0 : ℝ) 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)) :
    f (z₀ + z₁) = f z₀ + z₁ • ∫ t in (0 : ℝ)..1, f' (z₀ + t • z₁) := by
  rw [← sub_eq_iff_eq_add']
  let γ (t : ℝ) : C := z₀ + t • z₁
  have hint : IntervalIntegrable (z₁ • (f' ∘ γ)) MeasureTheory.volume 0 1 :=
    (ContinuousOn.const_smul hcont z₁).intervalIntegrable_of_Icc zero_le_one
  have hderiv' : ∀ t ∈ Set.uIcc (0 : ℝ) 1, HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
  · intro t ht
    refine (hderiv t <| (Set.uIcc_of_le (α := ℝ) zero_le_one).symm ▸ ht).scomp t ?_
    have : HasDerivAt (fun t : ℝ ↦ t • z₁) z₁ t
    · convert (hasDerivAt_id t).smul_const (F := C) _ using 1
      simp only [one_smul]
    exact this.const_add z₀
  convert (integral_eq_sub_of_hasDerivAt hderiv' hint).symm using 1
  · simp only [Function.comp_apply, one_smul, zero_smul, add_zero]
  · simp_rw [← integral_smul, Function.comp_apply]

This directly applies in my use case.

Is there some part of the naming convention that would apply to statements of the form f (x + y) = f x + ... with a variable f?
I guess one could state it in the form f (x + y) - f x = ... and call it intervalIntegral_sub_eq_integral_unitInterval or some such. Opinions?

[Michael Stoll]

@Heather Macbeth

[Michael Stoll]

Ruben Van de Velde said:

Does this help?

import Mathlib
lemma _HasDerivAt.comp_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] (a x : 𝕜) {𝕜' : Type u_1}
    [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h' : 𝕜'}
    (hh : HasDerivAt h h' (a + x)) :
    HasDerivAt (fun x ↦ h (a + x)) h' x  := by
  have : HasDerivAt (fun x ↦ (a + x)) _ x := hasDerivAt_id' x |>.const_add a
  have := HasDerivAt.scomp  (𝕜 := 𝕜) x hh this
  simpa [Function.comp_def] using this

I've golfed this down to

/-- Translation in the domain does not change the derivative. -/
lemma HasDerivAt.comp_const_add {𝕜 : Type*} [NontriviallyNormedField 𝕜] (a x : 𝕜) {𝕜' : Type*}
    [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h' : 𝕜'}
    (hh : HasDerivAt h h' (a + x)) :
    HasDerivAt (fun x ↦ h (a + x)) h' x  := by
  simpa [Function.comp_def] using HasDerivAt.scomp (𝕜 := 𝕜) x hh <| hasDerivAt_id' x |>.const_add a

/-- Translation in the domain does not change the derivative. -/
lemma HasDerivAt.comp_add_const {𝕜 : Type*} [NontriviallyNormedField 𝕜] (x a : 𝕜) {𝕜' : Type*}
    [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h' : 𝕜'}
    (hh : HasDerivAt h h' (x + a)) :
    HasDerivAt (fun x ↦ h (x + a)) h' x  := by
  simpa [Function.comp_def] using HasDerivAt.scomp (𝕜 := 𝕜) x hh <| hasDerivAt_id' x |>.add_const a

and would now like to PR these lemmas. But I find it hard to find a good home for these. They need Analysis.Calculus.Deriv.{Add|Comp}. It seems that Analysis.Calculus.LineDeriv.Basic is about the only file that imports both, but this does not really seem appropriate. Should I make a new file ...Deriv.Shift or so?

[Ruben Van de Velde]

Files are pretty cheap. How about you do that and anyone who disagrees can comment on the pr

[Michael Stoll]

#8614

[Michael Stoll]

#8615 for the unit interval version of the Fundamental Theorem of Calculus (xyz in an earlier message).

[Michael Stoll]

I'm using this to prove

lemma log_sub_logTaylor_norm_le (n : ℕ) {z : ℂ} (hz : ‖z‖ < 1) :
    ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (n + 1)

where logTaylor n z is the value of the nth Taylor polynomial of log (1+z) at the point z.
This is now in the file ComplexLog.lean here.

[Michael Stoll]

Next PR is #9116, which (since I found it useful in my code) introduces a definition Complex.slitPlane for the set of complex numbers minus the closed negative real axis and proves some API lemmas. The PR also replaces conditions of the form 0 < x.re ∨ x.im ≠ 0 by x ∈ slitPlane in a bunch of files (and fixes the resulting failures in proofs). It has passed CI just now. Comments are welcome!