arXiv subjects

Moritz Doll

Publications and source records attributed to Moritz Doll.

13 recordsLinked to original sources

arXiv2026

Foundations of Machine-Checked Control Theory in Lean

We introduce an open-source library for machine-checked control theory in the interactive proof assistant Lean to lay foundations for the verification of cyber-physical systems. To this end, as representative theorems, we present formalizations of Lyapunov stability theory and the small-gain theorem. First, the machinery employed for formalizing Lyapunov stability, i.e., neighborhood filters, allows stating a Lyapunov theorem that covers both points and sets and applies to continuous, discrete, and hybrid systems. Second, the small-gain theorem is proved via stating input-output systems as relations without the usual well-posedness assumption. The Lean formalization of each of these theorems is then presented. We conclude by discussing the library architecture and mentioning some of the other system theoretic results that are formalized in the library along with future plans.

math.OC↗

arXiv2026

The divisor of the twisted Selberg zeta function

For the Selberg zeta function of geometrically finite infinite-area hyperbolic orbisurfaces with twists by finite-dimensional unitary representations, we establish a factorization formula in terms of a Weierstrass product of the Laplace resonances of the considered hyperbolic orbisurface, Barnes G-functions, gamma functions, and the singularity degrees of the representation. We thereby provide an interpretation of the zeros and poles of the Selberg zeta function by spectral and geometric entities of the orbisurface and the representation. This formula generalizes the factorization result by Borthwick, Judge and Perry to hyperbolic orbisurfaces with orbifold singularities as well as to unitary twists. Also in the untwisted case, the presence of orbifold singularities yields a separate, previously unobserved contribution to the factorization formula.

math.SP↗

arXiv2025

Formalizing Schwartz functions and tempered distributions

Distribution theory is a cornerstone of the theory of partial differential equations. We report on the progress of formalizing the theory of tempered distributions in the interactive proof assistant Lean, which is the first formalization in any proof assistant. We give an overview of the mathematical theory and highlight key aspects of the formalization that differ from the classical presentation. As an application, we prove that the Fourier transform extends to a linear isometry on $L^2$ and we define Sobolev spaces via the Fourier transform on tempered distributions.

cs.LO↗

arXiv2025

The Klein-Gordon equation on asymptotically Minkowski spacetimes: the Feynman propagator

We develop a theory of Feynman propagators for the massive Klein--Gordon equation with asymptotically static perturbations. Building on our previous work on the causal propagators, we employ a framework based on propagation of singularities estimates in Vasy's 3sc-calculus. We combine these estimates to prove global spacetime mapping properties for the Feynman propagator, and to show that it satisfies a microlocal Hadamard condition. We show that the Feynman propagator can be realized as the inverse of a mapping between appropriate $L^2$-based Sobolev spaces with additional regularity near the asymptotic sources of the Hamiltonian flow, realized as a family of radial points on a compactified spacetime.

math.AP↗

arXiv2024

The Klein-Gordon equation on asymptotically Minkowski spacetimes: causal propagators

We construct the causal (forward/backward) propagators for the massive Klein-Gordon equation perturbed by a first order operator which decays in space but not necessarily in time. In particular, we obtain global estimates for forward/backward solutions to the inhomogeneous, perturbed Klein-Gordon equation, including in the presence of bound states of the limiting spatial Hamiltonians. To this end, we prove propagation of singularities estimates in all regions of infinity (spatial, null, and causal) and use the estimates to prove that the Klein-Gordon operator is an invertible mapping between adapted weighted Sobolev spaces. This builds off work of Vasy in which inverses of hyperbolic PDEs are obtained via construction of a Fredholm mapping problem using radial points propagation estimates. To deal with the presence of a perturbation which persists in time, we employ a class of pseudodifferential operators first explored in Vasy's many-body work.

math.AP↗

arXiv2022

Scattering Theory with Unitary Twists

We study the spectral properties of the Laplace operator associated to a hyperbolic surface in the presence of a unitary representation of the fundamental group. Following the approach by Guillop\'e and Zworski, we establish a factorization formula for the twisted scattering determinant and describe the behavior of the scattering matrix in a neighborhood of $1/2$.

math.SP↗

arXiv2021

Counting Resonances on Hyperbolic Surfaces with Unitary Twists

We present the Laplace operator associated to a hyperbolic surface $\Gamma\setminus\mathbb{H}$ and a unitary representation of the fundamental group $\Gamma$, extending the previous definition for hyperbolic surfaces of finite area to those of infinite area. We show that the resolvent of this operator admits a meromorphic continuation to all of $\mathbb{C}$ by constructing a parametrix for the Laplacian, following the approach by Guillop\'e and Zworski. We use the construction to provide an optimal upper bound for the counting function of the poles of the continued resolvent.

math.SP↗

arXiv2019

Weyl Law on Asymptotically Euclidean Manifolds

We study the asymptotic behaviour of the eigenvalue counting function for self-adjoint elliptic linear operators defined through classical weighted symbols of order $(1,1)$, on an asymptotically Euclidean manifold. We first prove a two term Weyl formula, improving previously known remainder estimates. Subsequently, we show that under a geometric assumption on the Hamiltonian flow at infinity there is a refined Weyl asymptotics with three terms. The proof of the theorem uses a careful analysis of the flow behaviour in the corner component of the boundary of the double compactification of the cotangent bundle. Finally, we illustrate the results by analysing the operator $Q=(1+|x|^2)(1-\Delta)$ on $\mathbb{R}^d$.

math.FA↗

arXiv2019

A Partial Data Problem in Linear Elasticity

We discuss the determination of the Lam\'e parameters of an elastic material by the means of boundary measurements. We will combine previous results of Eskin-Ralston and Isakov to prove inverse results in the case of bounded domains with partial data. Moreover, we generalise these results to infinite cylinders.

math.AP↗

arXiv2018

Schr\"odinger Trace Invariants for Homogeneous Perturbations of the Harmonic Oscillator

Let $H = H_0 + P$ denote the harmonic oscillator on $\mathbb{R}^d$ perturbed by an isotropic pseudodifferential operator $P$ of order $1$ and let $U(t) = \operatorname{exp}(- it H)$. We prove a Gutzwiller-Duistermaat-Guillemin type trace formula for $\operatorname{Tr} U(t)$. The singularities occur at times $t \in 2 \pi \mathbb{Z}$ and the coefficients involve the dynamics of the Hamilton flow of the symbol $\sigma(P)$ on the space $\mathbb{CP}^{d-1}$ of harmonic oscillator orbits of energy $1$. This is a novel kind of sub-principal symbol effect on the trace. We generalize the averaging technique of Weinstein and Guillemin to this order of perturbation, and then present two completely different calculations of $\operatorname{Tr} U(t)$. The first proof directly constructs a parametrix of $U(t)$ in the isotropic calculus, following earlier work of Doll-Gannot-Wunsch. The second proof conjugates the trace to the Bargmann-Fock setting, the order $1$ of the perturbation coincides with the `central limit scaling' studied by Zelditch-Zhou for Toeplitz operators.

math.AP↗

arXiv2018

Lagrangian distributions on asymptotically Euclidean manifolds

We develop the notion of Lagrangian distribution on scattering manifolds, meaning on the compactified cotangent bundle, which is a manifold with corners equipped with a scattering symplectic structure. In particular, we study the notion of principal symbol of the arising class of distributions.

math.AP↗

arXiv2017

Recurrence of singularities for second order isotropic pseudodifferential operators

Let $H$ be a self-adjoint isotropic elliptic pseudodifferential operator of order $2$. Denote by $u(t)$ the solution of the Schr\"odinger equation $(i\partial_t - H)u = 0$ with initial data $u(0) = u_0$. If $u_0$ is compactly supported the solution $u(t)$ is smooth for small $t > 0$, but not for all $t$. We determine the wavefront set of $u(t)$ in terms of the wavefront set of $u_0$ and the principal and subprincipal symbol of $H$.

math.AP↗

arXiv2017

Refined Weyl law for homogeneous perturbations of the harmonic oscillator

Let $H$ denote the harmonic oscillator Hamiltonian on $\mathbb{R}^d,$ perturbed by an isotropic pseudodifferential operator of order $1.$ We consider the Schr\"odinger propagator $U(t)=e^{-itH},$ and find that while $\operatorname{singsupp} \operatorname{Tr} U(t) \subset 2 \pi \mathbb{Z}$ as in the unperturbed case, there exists a large class of perturbations in dimension $d \geq 2$ for which the singularities of $\operatorname{Tr} U(t)$ at nonzero multiples of $2 \pi$ are weaker than the singularity at $t=0$. The remainder term in the Weyl law is of order $o(\lambda^{d-1})$, improving in these cases the $O(\lambda^{d-1})$ remainder previously established by Helffer--Robert.

math.AP↗