Imports
/-
Copyright (c) 2026 Adam Bornemann. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam Bornemann
-/
module
public import Mathlib.Analysis.Calculus.Deriv.Pow
public import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
public import Mathlib.Analysis.Distribution.TemperateGrowth
public import Mathlib.Analysis.Normed.Algebra.GelfandFormulaTemperate growth of the resolvent of a non-real complex number
i. Overview
For z : ℂ with z.im ≠ 0, every real number lies in the ℝ-resolvent set of z, so
Mathlib's algebra resolvent resolvent (R := ℝ) z = fun t : ℝ ↦ Ring.inverse (↑t - z) is a
globally defined, smooth map ℝ → ℂ. Its iterated derivatives have the closed form
(-1)ⁿ · n! · (resolvent z)ⁿ⁺¹ and are globally bounded by n! · (|z.im| ^ (n+1))⁻¹;
consequently the resolvent has temperate growth.
Smoothness and temperate growth are fun_prop lemmas, so composed variants such as the
affine reciprocal t ↦ (z + a·t)⁻¹ = resolvent (-z) (a·t) follow at call sites by
fun_prop.
ii. Key results
mem_resolventSet_of_im_ne_zero / resolventSet_eq_univ : every t : ℝ lies in
resolventSet ℝ z when z.im ≠ 0, i.e. t - z is invertible for all real t.
norm_resolvent_le : the global bound ‖resolvent z t‖ ≤ |z.im|⁻¹.
iteratedDeriv_resolvent : the closed form
iteratedDeriv n (resolvent z) = (-1)ⁿ · n! · (resolvent z)ⁿ⁺¹.
norm_iteratedDeriv_resolvent_le : the explicit derivative bounds
‖iteratedDeriv n (resolvent z) t‖ ≤ n! · (|z.im| ^ (n+1))⁻¹.
contDiff_resolvent, hasTemperateGrowth_resolvent : smoothness and temperate growth
along ℝ, both tagged @[fun_prop].
iii. Table of contents
A. The resolvent of a non-real complex number along ℝ
iv. References
@[expose] public section
A. The resolvent of a non-real complex number along ℝ
Every real number lies in the ℝ-resolvent set of a non-real complex number:
t - z is invertible for all t : ℝ.
z:ℂhz:z.im ≠ 0t:ℝ⊢ (algebraMap ℝ ℂ) t - z ≠ 0
exact fun h ↦ hz (z:ℂhz:z.im ≠ 0t:ℝh:(algebraMap ℝ ℂ) t - z = 0⊢ z.im = 0 All goals completed! 🐙)
The ℝ-resolvent set of a non-real complex number is all of ℝ.
lemma resolventSet_eq_univ (hz : z.im ≠ 0) : resolventSet ℝ z = Set.univ :=
Set.eq_univ_of_forall (mem_resolventSet_of_im_ne_zero hz)
The resolvent is globally bounded by |z.im|⁻¹: the imaginary part of the denominator
t - z is exactly -z.im.
z:ℂhz:z.im ≠ 0t:ℝ⊢ ‖(algebraMap ℝ ℂ) t - z‖⁻¹ ≤ |z.im|⁻¹
exact inv_anti₀ (abs_pos.mpr hz) (z:ℂhz:z.im ≠ 0t:ℝ⊢ |z.im| ≤ ‖(algebraMap ℝ ℂ) t - z‖ All goals completed! 🐙)
The resolvent of a non-real complex number is smooth along ℝ.
z:ℂhz:z.im ≠ 0this:resolvent z = fun t => (↑t - z)⁻¹⊢ ContDiff ℝ ∞ fun t => (↑t - z)⁻¹
All goals completed! 🐙
Closed form for the iterated derivatives of the resolvent: the n-th derivative is
(-1)ⁿ · n! · (resolvent z)ⁿ⁺¹.
z:ℂhz:z.im ≠ 0n:ℕih:iteratedDeriv n (resolvent z) = fun t => (-1) ^ n * ↑n ! * resolvent z t ^ (n + 1)t:ℝhd:HasDerivAt (fun y => (-1) ^ n * ↑n ! * resolvent z y ^ (n + 1))
((-1) ^ n * ↑n ! * (↑(n + 1) * resolvent z t ^ (n + 1 - 1) * -resolvent z t ^ 2)) t⊢ (-1) ^ n * ↑n ! * (↑(n + 1) * resolvent z t ^ (n + 1 - 1) * -resolvent z t ^ 2) =
(-1) ^ (n + 1) * ↑(n + 1)! * resolvent z t ^ (n + 1 + 1)
z:ℂhz:z.im ≠ 0n:ℕih:iteratedDeriv n (resolvent z) = fun t => (-1) ^ n * ↑n ! * resolvent z t ^ (n + 1)t:ℝhd:HasDerivAt (fun y => (-1) ^ n * ↑n ! * resolvent z y ^ (n + 1))
((-1) ^ n * ↑n ! * (↑(n + 1) * resolvent z t ^ (n + 1 - 1) * -resolvent z t ^ 2)) t⊢ (-1) ^ n * ↑n ! * ((↑n + 1) * resolvent z t ^ n * -resolvent z t ^ 2) =
(-1) ^ (n + 1) * ((↑n + 1) * ↑n !) * resolvent z t ^ (n + 1 + 1)
All goals completed! 🐙
Every iterated derivative of the resolvent is globally bounded, explicitly by
n! · (|z.im| ^ (n + 1))⁻¹.
z:ℂhz:z.im ≠ 0n:ℕt:ℝ⊢ ↑n ! * ‖resolvent z t‖ ^ (n + 1) ≤ ↑n ! * |z.im|⁻¹ ^ (n + 1)
z:ℂhz:z.im ≠ 0n:ℕt:ℝ⊢ ‖resolvent z t‖ ≤ |z.im|⁻¹
All goals completed! 🐙
The resolvent of a non-real complex number has temperate growth along ℝ.
z:ℂhz:z.im ≠ 0n:ℕt:ℝ⊢ ‖iteratedDeriv n (resolvent z) t‖ ≤ ↑n ! * (|z.im| ^ (n + 1))⁻¹
All goals completed! 🐙