LOGOS Seminar

Who wants to give talks when?

In this talk I will present a joint work with Mathias Braun, in which we prove a synthetic version of the Gannon-Lee incompleteness theorem. We assume the recent synthetic characterization of trappedness and of the null energy condition by Ketterer, instead of the classical hypoteses. I will start with an introduction on the incompleteness theorems of general relativity and the classical Gannon-Lee Theorem, and then I will describe Ketterer's conditions and state our synthetic Gannon-Lee Theorem. If time allows, I will briefly discuss where our proof differs from the classical one and how we apply the synthetic conditions. password for the recording @4!S&N2k

A Proof Assistant is a software environment that allows the composition of formalized mathematical theorems and proofs in a format that makes the proofs mechanically verifiable. Recently, a spotlight has been shining on the Lean Proof Assistant and its project Mathlib, aiming to build a unified library of formalized mathematics at the level of current research. I will give a quick and informal introduction to Lean’s formal language (Dependent Type Theory) and how it encodes logical statements/proofs, guided by the questions I myself had when first learning it. I will follow it up by a small practical demonstration. Along the way, I will try to highlight the opportunities and challenges that formalized proofs offer to mathematicians today.

We examine a class of semi-Riemannian manifolds that undergo smooth metric signature change from - Riemannian to Lorentzian — across a hypersurface with a transverse radical. This class includes physically motivated cosmological models such as the Hartle-Hawking “no-boundary” proposal, in which the universe transitions smoothly from a Euclidean to a Lorentzian phase. We show that these manifolds admit isometric embeddings into higher-dimensional pseudo Euclidean spaces and, in particular, prove the existence of global isometric embeddings of the canonical model into both Minkowski and Misner spaces. This framework provides a mathematical setting for studying smooth signature change and its role in higher-dimensional and cosmological models.

The uncertainty principle in harmonic analysis states that a non-zero function and its Fourier transform cannot be simultaneously too sharply localized. There are numerous precise mathematical formulations of this meta-theorem. Beurling’s own version of the uncertainty principle for Fourier transforms is the following clean and elegant statement: given $f \in L^{1}(\mathbb{R})$, $$ \iint_{\mathbb{R}^{2}} \bigl|f(x)\,\widehat{f}(\xi)\bigr|\, e^{\,|x\cdot \xi|}\, dx\, d\xi < \infty \;\Rightarrow\; f=0. $$ The goal of this talk is to present a general quantified version of Beurling's uncertainty principle. We will characterize in several ways those functions $f \in L^{1}(\mathbb{R}^{n})$ such that $$ \iint_{\mathbb{R}^{2n}} \frac{\bigl|f(x)\,\widehat{f}(\xi)\bigr|\, e^{\,|x\cdot \xi|}}{W\!\bigl(|x|+|\xi|\bigr)} \, dx\, d\xi < \infty, $$ where $W:[0,\infty)\to[1,\infty)$ is an unbounded non-decreasing function subject to certain natural regularity conditions. The talk is based on collaborative work with Lenny Neyt.