Physlib.Mathematics.Resolvent

Temperate 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

A. The resolvent of a non-real complex number along `ℝ`

7 declarations

theorem

Real numbers belong to the resolvent set of non-real complex numbers

#mem_resolventSet_of_im_ne_zero

Let $z$ be a complex number such that its imaginary part is non-zero ( $\text{Im}(z) \neq 0$ ). For every real number $t \in \mathbb{R}$ , $t$ belongs to the resolvent set of $z$ over $\mathbb{R}$ . This means that the value $t - z$ is invertible for all $t \in \mathbb{R}$ .

theorem

$\text{resolventSet}_{\mathbb{R}}(z) = \mathbb{R}$ for $z$ with $\text{Im}(z) \neq 0$

#resolventSet_eq_univ

Let $z$ be a complex number such that its imaginary part $\text{Im}(z) \neq 0$ . Then the $\mathbb{R}$ -resolvent set of $z$ (the set of real numbers $t$ such that $t - z$ is invertible in $\mathbb{C}$ ) is equal to the set of all real numbers $\mathbb{R}$ .

theorem

The norm of the resolvent is bounded by $|\text{Im}(z)|^{-1}$

#norm_resolvent_le

Let $z \in \mathbb{C}$ be a complex number with a non-zero imaginary part, $\text{Im}(z) \neq 0$ . For any real number $t \in \mathbb{R}$ , the norm of the resolvent $(t - z)^{-1}$ is globally bounded by the reciprocal of the absolute value of the imaginary part of $z$ : $\| (t - z)^{-1} \| \leq \frac{1}{|\text{Im}(z)|}$

theorem

The Resolvent of a Complex Number $z$ with $\text{Im}(z) \neq 0$ is Smooth on $\mathbb{R}$

#contDiff_resolvent

For any complex number $z$ with a non-zero imaginary part ( $\text{Im}(z) \neq 0$ ), the resolvent function $f: \mathbb{R} \to \mathbb{C}$ defined by $f(t) = (t - z)^{-1}$ is infinitely differentiable (smooth) on $\mathbb{R}$ .

theorem

$n$ -th Derivative of the Resolvent of $z \in \mathbb{C} \setminus \mathbb{R}$

#iteratedDeriv_resolvent

Let $z$ be a complex number with a non-zero imaginary part ( $\text{Im}(z) \neq 0$ ). The resolvent function $\text{resolvent}(z) : \mathbb{R} \to \mathbb{C}$ is defined as $\text{resolvent}(z)(t) = (t - z)^{-1}$ . For any natural number $n$ , the $n$ -th iterated derivative of this resolvent function is given by: $\frac{d^n}{dt^n} (\text{resolvent}(z)(t)) = (-1)^n n! (\text{resolvent}(z)(t))^{n+1}$ which is equivalent to: $\frac{d^n}{dt^n} \left( \frac{1}{t - z} \right) = \frac{(-1)^n n!}{(t - z)^{n+1}}$

theorem

$\| \frac{d^n}{dt^n} (t - z)^{-1} \| \leq n! \cdot |\text{Im}(z)|^{-(n+1)}$

#norm_iteratedDeriv_resolvent_le

Let $z \in \mathbb{C}$ be a complex number with a non-zero imaginary part ( $\text{Im}(z) \neq 0$ ). For any natural number $n \in \mathbb{N}$ and any real number $t \in \mathbb{R}$ , the norm of the $n$ -th derivative of the resolvent function $R_z(t) = \frac{1}{t - z}$ is bounded by: $\left\| \frac{d^n}{dt^n} \left( \frac{1}{t - z} \right) \right\| \leq \frac{n!}{|\text{Im}(z)|^{n+1}}$ where $|\text{Im}(z)|$ denotes the absolute value of the imaginary part of $z$ .

theorem

The Resolvent of $z$ with $\text{Im}(z) \neq 0$ has Temperate Growth

#hasTemperateGrowth_resolvent

For any complex number $z$ such that its imaginary part is non-zero ( $\text{Im}(z) \neq 0$ ), the resolvent function $f : \mathbb{R} \to \mathbb{C}$ defined by $f(t) = (t - z)^{-1}$ has temperate growth.

Physlib.Mathematics.Resolvent

Temperate growth of the resolvent of a non-real complex number

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. The resolvent of a non-real complex number along `ℝ`

Real numbers belong to the resolvent set of non-real complex numbers

resolventSetR(z)=R\text{resolventSet}_{\mathbb{R}}(z) = \mathbb{R}resolventSetR​(z)=R for zzz with Im(z)≠0\text{Im}(z) \neq 0Im(z)=0

The norm of the resolvent is bounded by ∣Im(z)∣−1|\text{Im}(z)|^{-1}∣Im(z)∣−1

The Resolvent of a Complex Number zzz with Im(z)≠0\text{Im}(z) \neq 0Im(z)=0 is Smooth on R\mathbb{R}R

nnn-th Derivative of the Resolvent of z∈C∖Rz \in \mathbb{C} \setminus \mathbb{R}z∈C∖R

∥dndtn(t−z)−1∥≤n!⋅∣Im(z)∣−(n+1)\| \frac{d^n}{dt^n} (t - z)^{-1} \| \leq n! \cdot |\text{Im}(z)|^{-(n+1)}∥dtndn​(t−z)−1∥≤n!⋅∣Im(z)∣−(n+1)

The Resolvent of zzz with Im(z)≠0\text{Im}(z) \neq 0Im(z)=0 has Temperate Growth

$\text{resolventSet}_{\mathbb{R}}(z) = \mathbb{R}$ for $z$ with $\text{Im}(z) \neq 0$

The norm of the resolvent is bounded by $|\text{Im}(z)|^{-1}$

The Resolvent of a Complex Number $z$ with $\text{Im}(z) \neq 0$ is Smooth on $\mathbb{R}$

$n$ -th Derivative of the Resolvent of $z \in \mathbb{C} \setminus \mathbb{R}$

$\| \frac{d^n}{dt^n} (t - z)^{-1} \| \leq n! \cdot |\text{Im}(z)|^{-(n+1)}$

The Resolvent of $z$ with $\text{Im}(z) \neq 0$ has Temperate Growth