deriv of sin z / z at 0 (ℂ)

Stream: mathlib4

[Bob Jefferson]

Can anyone help with a lemma? Lean version 4.27.0-rc1, mathlib commit: 9ffe92940ecaeb3dcd538bc6e1644e60c32d4561

I have defined

def sinDiv (z : ℂ) : ℂ := if z = 0 then 1 else Complex.sin z / z

and I have already proved Continuous sinDiv.

What I want is:

lemma deriv_sinDiv_zero : deriv sinDiv 0 = (0 : ℂ)

Mathematically this is trivial, but in this snapshot I cannot find a suitable lemma expressing the higher-order behaviour of sin at 0.

Facts I do have / found:

• hasDerivAt_sin 0
• isEquivalent_sin : sin ~[𝓝 0] id
• analyticAt_sin
• Complex.hasSum_sin / Complex.sin_eq_tsum

What I cannot find (despite extensive searching with rg):

• any lemma of the form (sin z - z) = o(z^2)
• or (sin z / z - 1) = o(z)
• or a ready-made derivative lemma for sinc / sin z / z at 0

I’ve checked:

• Analysis/SpecialFunctions/Trigonometric/Deriv.lean
• Series.lean
• Sinc.lean

Question:
Is there an existing lemma in mathlib that directly gives
deriv (fun z => sin z / z) 0 = 0 (or equivalent HasDerivAt) over ℂ, or a standard lemma expressing the second-order vanishing of sin z - z at 0?

If so, what is the intended lemma name / path? Thanks in advance.

[Vlad Tsyrklevich]

I'd recommend using loogle instead of text search.

[Vlad Tsyrklevich]

(deleted)

[Vlad Tsyrklevich]

@loogle Complex.sin, "deriv"

[loogle]

:search: Complex.logDeriv_sin, Complex.deriv_sin, and 36 more

[Vlad Tsyrklevich]

Complex.iteratedDeriv_even_sin seems like it might what you're looking for, at least w.r.t. the second order derivative

[Bob Jefferson]

Thanks, that makes sense conceptually, the vanishing of even iterated derivatives is exactly the “no linear term in sin z / z” idea.

I’m still missing the plumbing step in this snapshot though. I couldn’t get a usable statement out of it via #check in my project context (I might be importing the wrong file, or the lemma is in a namespace I’m not opening correctly).

Could you confirm:

1. Which import brings it into scope? Is it Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (or ComplexDeriv)?

2. What is the exact type/signature you see for Complex.iteratedDeriv_even_sin? (I want to specialize it to get something like iteratedDeriv 2 Complex.sin 0 = 0.)

3. Once we have iteratedDeriv 2 Complex.sin 0 = 0, what’s the intended lemma to turn that into
   deriv (fun z => (if z = 0 then 1 else Complex.sin z / z)) 0 = 0?
   Is the intended route via HasFPowerSeriesAt/Taylor coefficients, or is there a lemma relating deriv (fun z => sin z / z) directly to iteratedDeriv 2 sin at 0?

[Bob Jefferson]

For info, I checked the online docs for Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv: they do show

• Complex.hasDerivAt_sin and Complex.hasStrictDerivAt_sin, and

• Complex.isEquivalent_sin : Asymptotics.IsEquivalent (nhds 0) sin id.

So the first-order behaviour and basic derivatives are exposed in this namespace.

However, I don’t see any documented lemma here connecting iteratedDeriv or the second derivative of sin at 0 to a Taylor expansion or a derivative of sin z / z at 0. The docs page doesn’t mention iteratedDeriv_even_sin, or a way to extract Taylor coefficients from power series or derivatives in this snapshot.

Could someone point me to the exact lemma name or file where Complex.iteratedDeriv_even_sin lives (and how to turn it into a usable statement about deriv (fun z => sin z / z) 0)? Is it a different namespace / import I’m missing?

[Bob Jefferson]

I can confirm that
Complex.iteratedDeriv_even_sin (in Analysis/SpecialFunctions/Trigonometric/Deriv.lean) gives the exact formula for even derivatives, e.g.

iteratedDeriv (2 * n) sin = (-1)^n * sin

and similarly for odd derivatives. So the second derivative / higher derivatives side is clear.

What I’m missing, though, is a ready-made asymptotic / limit lemma for the cubic remainder at 0. Concretely, I’m trying to prove something like

Filter.Tendsto (fun z : ℂ => (Complex.sin z - z) / z^3) (nhdsWithin 0 {0}ᶜ) (nhds (-(1/6)))

(or equivalently sin z - z = O(z^3) / = o(z^2) near 0).

I searched through:

• Analysis/SpecialFunctions/Trigonometric/Deriv.lean

• DerivHyp.lean

• Series.lean

• Sinc.lean

and only found the first-order result

theorem isEquivalent_sin : sin ~[𝓝 0] id

but nothing packaging the cubic remainder.

I can prove this directly from the power series using
Complex.sin_eq_tsum / Complex.hasSum_sin in Trigonometric/Series.lean
(by splitting off the first two terms and bounding the tail), and I’m happy to do that if needed.
Before re-proving it, I just wanted to check whether there is an existing lemma for the cubic Taylor remainder / (sin z - z) / z^3 limit in this mathlib snapshot that I’ve missed.

[Bob Jefferson]

For the record, I ended up switching to a series-based approach, which worked out better in any case. Appreciate the help, nevertheless.

[Bhavik Mehta]

I noticed that we have docs#Real.sin_bound, but the proof essentially works for docs#Complex.sin, and that version should help prove your result and give a simpler proof of docs#Real.sin_bound too. I'm preparing a PR now, but the main statement is

theorem Complex.sin_bound {x : ℂ} (hx : ‖x‖ ≤ 1) : ‖sin x - (x - x ^ 3 / 6)‖ ≤ ‖x‖ ^ 4 * (5 / 96) :=

In particular, while this is a weaker bound than what you get with the Taylor series, it can be proved earlier in mathlib, and gives slightly more control than what I think you need?

[Bob Jefferson]

That’s extremely helpful, thank you — this is exactly the kind of lemma I was hoping existed.

My immediate goal is to prove the punctured-neighbourhood cubic limit

Tendsto (fun z : ℂ => (Complex.sin z - z) / z^3) (𝓝[≠] 0) (𝓝 (-(1/6)))

and your bound gives this almost for free, since it implies
(Complex.sin z - (z - z^3/6)) / z^3 → 0 as z → 0.

So a lemma of the form

theorem Complex.sin_bound {x : ℂ} (hx : ‖x‖ ≤ 1) : ‖Complex.sin x - (x - x ^ 3 / 6)‖ ≤ ‖x‖ ^ 4 * (5 / 96)

would be perfect for my use case.

I’m very happy to depend on this lemma rather than reproving the Taylor remainder via series tails. If you’re able to expose it as Complex.sin_bound (or something similar), I can adapt my development immediately.

[Bhavik Mehta]

This lemma and the cos version are here: #34350

[Bob Jefferson]

Yes, that lemma is exactly what I need. My goal is to show

Tendsto (fun z : ℂ => (Complex.sin z - z) / z^3) (𝓝[≠] 0) (𝓝 (-(1/6)))

and your bound implies immediately that
(Complex.sin z - (z - z^3/6)) / z^3 → 0 as z → 0, so this is perfect.

I’ll switch my development to use Complex.sin_bound as soon as this PR is merged.
Thanks again — this simplifies things a lot and keeps the analytic input very clean.

[Jireh Loreaux]

I bet @Vasilii Nesterov 's compute_asymptotics can blast away your limit goal in one line, at least in the real case.

[Bob Jefferson]

Thanks! My goal is over ℂ rather than ℝ.
Does compute_asymptotics support complex functions already, or would I need to reduce to the real case first?

[Snir Broshi]

#28291 looks very specific to reals

[Bob Jefferson]

Thanks, that’s helpful to know. My goal is to prove the limit for the complex function

( \sin z - z ) / z^3 \to -1/6

along the punctured neighbourhood of 0, staying close to Euler’s series-based argument.

The new filter lemmas look useful for cleaning up the 𝓝[≠] 0 plumbing, but I’ll still need either a complex asymptotic tool or an explicit complex bound.

Do you know whether compute_asymptotics (or similar) currently works for complex functions like Complex.sin, or is it real-only for now?

[Yury G. Kudryashov]

Can you use general theory about Taylor series for this?

[Yury G. Kudryashov]

I mean, we know that for a holomorphic function, its Taylor series converges to it in the sense of HasFPowerSeriesOnBall, so we can use results about it.

[Bob Jefferson]

Thanks, that’s helpful. My aim with this project is to stay fairly Euler-faithful in spirit, i.e. work directly with the explicit sine series rather than switching immediately to the general holomorphic/Taylor machinery, which is why I’ve been doing things the hard way.

That said, your suggestion sounds like a good fallback if the tail estimates get too painful. Could you point me to the specific lemmas I should be looking for? In particular:

• is there already a HasFPowerSeriesOnBall statement for Complex.sin in mathlib?

• which lemma gives a remainder estimate of the form f z = p z + o(‖z‖^3) or O(‖z‖^4) from that?

Knowing the exact names would help me evaluate whether to switch approaches.

[Yury G. Kudryashov]

You can get HasFPowerSeriesOnBall for Complex.exp the same way we prove docs#analyticOn_cexp
Then you can use results from https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Analytic/Basic.html

[Snir Broshi]

Bob Jefferson said:

Thanks, that’s helpful to know. My goal is to prove the limit for the complex function
...
Do you know whether compute_asymptotics (or similar) currently works for complex functions like Complex.sin, or is it real-only for now?

I don't understand why you thanked me and then asked the same question again, but like I said it looks specific to reals

[Bob Jefferson]

Yes, sleep-deprivation mostly. That was 4 am in the UK.

My project needs the limit

(Complex.sin z - z)/z^3 \to -(1/6)

on 𝓝[≠] 0 for ℂ.

Given the new Complex.sin_bound PR, what is the simplest way to turn that inequality into a Filter.Tendsto statement in mathlib style?

(In particular: is there an existing lemma I should use to go from
‖f z‖ ≤ ‖z‖^4 * C
to
Tendsto (fun z => f z / z^3) (𝓝[≠] 0) (𝓝 0) ?)

[Junyan Xu]

Should we prove a version of l'Hopital's rule for (complex) analytic functions?

[Yury G. Kudryashov]

BTW, did you try asking AI like https://aristotle.harmonic.fun/ ?

[Bob Jefferson]

Junyan Xu said:

Should we prove a version of l'Hopital's rule for (complex) analytic functions?

I think l’Hôpital is overkill here. For Complex.sin we already have the power series and the remainder bounds (now also Complex.sin_bound). My immediate need is a Tendsto statement on 𝓝[≠] 0, and it looks like it should come from:

(a) Tendsto (fun z => z^k) (𝓝[≠] 0) (𝓝 0) for k>0,
(b) tendsto_const_nhds.mul / norm estimates, and
(c) tendsto_zero_of_norm_tendsto_zero / tendsto_principal style lemmas.

So I’m hoping to stay in the “series + bound → tendsto” lane rather than add a complex l’Hôpital rule.

[Bob Jefferson]

Yury G. Kudryashov said:

BTW, did you try asking AI like https://aristotle.harmonic.fun/ ?

I have been using AI to iterate on the Lean proof, but the main bottleneck is not generating code, it’s finding the right existing mathlib lemmas in this snapshot (many tsum_* conveniences are missing / renamed). Any pointers to the canonical lemma chain for “norm bound → Tendsto on 𝓝[≠] 0” would still be hugely appreciated.

[Bob Jefferson]

The simplest route I see is to avoid continuity of multiplication on ℂ entirely: prove a norm bound on the quotient, e.g. from ‖f z‖ ≤ C * ‖z‖^4 get ‖f z / z^3‖ ≤ C * ‖z‖ on z≠0, then use Tendsto (fun z => ‖z‖) (𝓝[≠] 0) (𝓝 0) and a squeeze lemma (tendsto_of_tendsto_of_tendsto_of_le_of_le or any norm-variant), and finally tendsto_zero_of_norm_tendsto_zero. Is there an existing lemma that turns an eventual bound ‖g z‖ ≤ h z plus Tendsto h … (𝓝 0) into Tendsto g … (𝓝 0)?

[Yury G. Kudryashov]

docs#squeeze_zero_norm'

[Yury G. Kudryashov]

@loogle Norm.norm, Filter.Eventually, LE.le, 0, Filter.Tendsto

[loogle]

:search: squeeze_one_norm', squeeze_zero_norm', and 2 more

[Bob Jefferson]

Thanks, squeeze_zero_norm' is exactly what I needed. I can avoid ContinuousMul and any Tendsto.mul on ℂ by proving an eventual bound on the norm and then applying squeeze_zero_norm'. Concretely, from ‖f z‖ ≤ C * ‖z‖^4 (eventually on 𝓝[≠] 0) and z ≠ 0 I get ‖f z / z^3‖ ≤ C * ‖z‖, then combine tendsto_norm_nhdsNE_zero with tendsto_const_nhds.mul (in ℝ) and finish with squeeze_zero_norm'. Much appreciated.

[Bob Jefferson]

Thanks everyone for your helpful suggestions. Greatly appreciated.

For the record, what worked in the end was to avoid continuity of multiplication and instead go via norm bounds and a squeeze argument. I proved the cubic expansion of Complex.sin by showing

(\sin z - z - (-(1/6)) z^3)/z^3 \to 0

on 𝓝[≠] 0, using dominated convergence on the normalized remainder series and then converting ‖f z‖ → 0 into f z → 0.

The lemmas that made this go through cleanly were:

• tendsto_zero_iff_norm_tendsto_zero,

• tendsto_tsum_of_dominated_convergence,

• and the squeeze-style lemmas in Analysis/Normed/Group/Continuity.

So this now gives:

Tendsto (fun z => (Complex.sin z - z) / z^3) (𝓝[≠] 0) (𝓝 (-(1/6)))

[Yury G. Kudryashov]

Here is a proof from Aristotle (for Lean/Mathlib v4.24.0, may need adjustments for the current version). It goes straight via the tsum definition, with almost no sin-specific theory.

theorem limit_sin_sub_id_div_pow_three : Filter.Tendsto (fun z : ℂ => (Complex.sin z - z) / z ^ 3) (nhdsWithin 0 {0}ᶜ) (nhds (-(1 / 6))) := by
  -- We'll use the fact that $\sin(z) = z - \frac{z^3}{6} + O(z^5)$ to simplify the expression.
  have h_sin_approx : ∀ z : ℂ, Complex.sin z = z - z^3 / 6 + z^5 * (∑' k : ℕ, ( (-1)^k * z^(2 * k)) / (Nat.factorial (2 * k + 5))) := by
    intro z
    rw [Complex.sin_eq_tsum];
    rw [ ← Summable.sum_add_tsum_nat_add 2 ];
    · norm_num [ Finset.sum_range_succ ];
      rw [ ← tsum_mul_left ] ; ring;
    · exact Summable.of_norm <| by simpa using Real.summable_pow_div_factorial _ |> Summable.comp_injective <| by intro m n h; simpa using h;
  -- Substitute the approximation into the expression.
  suffices h_subst : Filter.Tendsto (fun z : ℂ => (-1 / 6 + z^2 * (∑' k : ℕ, ((-1)^k * z^(2 * k)) / (Nat.factorial (2 * k + 5)))) : ℂ → ℂ) (nhdsWithin 0 {0}ᶜ) (nhds (-(1 / 6 : ℂ))) by
    refine' h_subst.congr' ( by filter_upwards [ self_mem_nhdsWithin ] with z hz using by rw [ h_sin_approx z ] ; rw [ eq_comm ] ; rw [ div_eq_iff ( pow_ne_zero _ hz ) ] ; ring );
  -- The series $\sum_{k=0}^{\infty} \frac{(-1)^k z^{2k}}{(2k+5)!}$ converges uniformly to an analytic function on any compact subset of $\mathbb{C}$.
  have h_series_uniform : ContinuousOn (fun z : ℂ => ∑' k : ℕ, ((-1)^k * z^(2 * k)) / (Nat.factorial (2 * k + 5))) (Metric.closedBall 0 1) := by
    refine' continuousOn_tsum _ _ _ <;> norm_num +zetaDelta at *;
    exacts [ fun n => ( 1 : ℝ ) / ( Nat.factorial ( 2 * n + 5 ) ), fun n => Continuous.continuousOn <| by continuity, by simpa using Summable.comp_injective ( Real.summable_pow_div_factorial 1 ) <| by intro m n h; simpa using h, fun n x hx => by simpa using div_le_div_of_nonneg_right ( pow_le_one₀ ( by positivity ) hx ) <| by positivity ];
  field_simp;
  exact tendsto_nhdsWithin_of_tendsto_nhds ( by convert Filter.Tendsto.div_const ( Filter.Tendsto.add tendsto_const_nhds <| Filter.Tendsto.mul ( tendsto_const_nhds.mul <| Filter.tendsto_id.pow 2 ) <| h_series_uniform.continuousAt ( Metric.closedBall_mem_nhds _ zero_lt_one ) ) _ using 2 ; norm_num )

[Bob Jefferson]

Thanks, that’s very helpful. My project goal is a Lean proof of Euler–Basel that tracks Euler’s product-and-coefficient comparison as closely as possible, so I’m using a small-z cubic remainder lemma in a very specific “drop-in” form for the product step. Your lemma looks like a great alternative derivation and a nice consistency check, and I may add a small bridge lemma showing equivalence once the main pipeline is finished.

[Bob Jefferson]

I wanted to check something about novelty before I go much further.

I’m working on a Lean formalisation of an Euler-style proof of the Basel problem, based on:

• the infinite product
sin(π z)/(π z) = ∏ (1 - z²/n²)
• a quadratic expansion of the LHS near z = 0,
• a quadratic expansion of the finite Euler product, and
• coefficient comparison as N → ∞ to extract ∑ 1/n² = π²/6.

In other words, I’m trying to mirror Euler’s original coefficient-comparison argument using the sine product, rather than going via Fourier series / Parseval / modern power series machinery.

Does anyone know of an existing Lean formalisation of this style of proof (sine product + coefficient comparison), or would this be new?
I know mathlib has a Basel proof, but as far as I can tell it goes via Fourier analysis.

Any pointers very welcome.