-
Carleson Operators on Doubling Metric Measure Spaces
Authors:
Lars Becker,
Floris van Doorn,
Asgar Jamneshan,
Rajula Srivastava,
Christoph Thiele
Abstract:
We prove a new generalization of a theorem of Carleson, namely bounds for a generalized Carleson operator on doubling metric measure spaces. Additionally, we explicitly reduce Carleson's classical result on pointwise convergence of Fourier series to this new theorem. Both proofs are presented in great detail, suitable as a blueprint for computer verification using the current capabilities of the s…
▽ More
We prove a new generalization of a theorem of Carleson, namely bounds for a generalized Carleson operator on doubling metric measure spaces. Additionally, we explicitly reduce Carleson's classical result on pointwise convergence of Fourier series to this new theorem. Both proofs are presented in great detail, suitable as a blueprint for computer verification using the current capabilities of the software package Lean. Note that even Carleson's classical result has not yet been computer-verified.
△ Less
Submitted 10 May, 2024;
originally announced May 2024.
-
Evaluating the performance of ionic liquid coatings for mitigation of spacecraft surface charges
Authors:
M. Wendt,
R. Lange,
F. Dorn,
J. Berdermann,
I. Barke,
S. Speller
Abstract:
To reduce the impact of charging effects on satellites, cheap and lightweight conductive coatings are desirable. We mimic space-like charging environments in ultra-high vacuum (UHV) chambers during deposition of charges via the electron beam of a scanning electron microscope (SEM). We use the charge induced signatures in SEM images of a thin ionic liquid (IL) film on insulating surfaces such as gl…
▽ More
To reduce the impact of charging effects on satellites, cheap and lightweight conductive coatings are desirable. We mimic space-like charging environments in ultra-high vacuum (UHV) chambers during deposition of charges via the electron beam of a scanning electron microscope (SEM). We use the charge induced signatures in SEM images of a thin ionic liquid (IL) film on insulating surfaces such as glass, to assess the general performance of such coatings. In order to get a reference structure in SEM, the samples were structured by nanosphere lithography and coated with IL. The IL film (we choose BMP DCA, due to its beneficial physical properties) was applied ex situ and a thickness of 10 to 30 nm was determined by reflectometry. Such an IL film is stable under vacuum conditions. It would also only lead to additional mass of below 20 mg/m$^2$. At about 5 A/m$^2 \approx 3\cdot10^{19}$ e/(s$\cdot$m$^2$), a typical sample charging rate in SEM, imaging is possible with no noticeable contrast changes over many hours; this electron current density is already 6 orders of magnitudes higher than "worst case geosynchronous environments" of $3\cdot10^{-6}$ A/m$^2$. Measurements of the surface potential are used for further insights in the reaction of IL films to the electron beam of a SEM. Participating mechanisms such as polarization or reorientation will are discussed.
△ Less
Submitted 4 September, 2023;
originally announced September 2023.
-
Formalising the $h$-principle and sphere eversion
Authors:
Patrick Massot,
Floris van Doorn,
Oliver Nash
Abstract:
In differential topology and geometry, the h-principle is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existence of a solution come from algebraic topology.
We describe a formalisation in Lean of the local h-principle for first-order, open, ample partial differential relations. This is a significant result in differential topo…
▽ More
In differential topology and geometry, the h-principle is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existence of a solution come from algebraic topology.
We describe a formalisation in Lean of the local h-principle for first-order, open, ample partial differential relations. This is a significant result in differential topology, originally proven by Gromov in 1973 as part of his swee** effort which greatly generalised many previous flexibility results in topology and geometry. In particular it reproves Smale's celebrated sphere eversion theorem, a visually striking and counter-intuitive construction. Our formalisation uses Theillière's implementation of convex integration from 2018.
This paper is the first part of the sphere eversion project, aiming to formalise the global version of the h-principle for open and ample first order differential relations, for maps between smooth manifolds. Our current local version for vector spaces is the main ingredient of this proof, and is sufficient to prove the titular corollary of the project. From a broader perspective, the goal of this project is to show that one can formalise advanced mathematics with a strongly geometric flavour and not only algebraically-flavoured
△ Less
Submitted 14 October, 2022;
originally announced October 2022.
-
Designing a general library for convolutions
Authors:
Floris van Doorn
Abstract:
We will discuss our experiences and design decisions obtained from building a formal library for the convolution of two functions. Convolution is a fundamental concept with applications throughout mathematics. We will focus on the design decisions we made to make the convolution general and easy to use, and the incorporation of this development in Lean's mathematical library mathlib.
We will discuss our experiences and design decisions obtained from building a formal library for the convolution of two functions. Convolution is a fundamental concept with applications throughout mathematics. We will focus on the design decisions we made to make the convolution general and easy to use, and the incorporation of this development in Lean's mathematical library mathlib.
△ Less
Submitted 14 October, 2022;
originally announced October 2022.
-
Formalized Haar Measure
Authors:
Floris van Doorn
Abstract:
We describe the formalization of the existence and uniqueness of Haar measure in the Lean theorem prover. The Haar measure is an invariant regular measure on locally compact groups, and it has not been formalized in a proof assistant before. We will also discuss the measure theory library in Lean's mathematical library \textsf{mathlib}, and discuss the construction of product measures and the proo…
▽ More
We describe the formalization of the existence and uniqueness of Haar measure in the Lean theorem prover. The Haar measure is an invariant regular measure on locally compact groups, and it has not been formalized in a proof assistant before. We will also discuss the measure theory library in Lean's mathematical library \textsf{mathlib}, and discuss the construction of product measures and the proof of Fubini's theorem for the Bochner integral.
△ Less
Submitted 4 February, 2021;
originally announced February 2021.
-
A Formal Proof of the Independence of the Continuum Hypothesis
Authors:
Jesse Michael Han,
Floris van Doorn
Abstract:
We describe a formal proof of the independence of the continuum hypothesis ($\mathsf{CH}$) in the Lean theorem prover. We use Boolean-valued models to give forcing arguments for both directions, using Cohen forcing for the consistency of $\neg \mathsf{CH}$ and a $σ$-closed forcing for the consistency of $\mathsf{CH}$.
We describe a formal proof of the independence of the continuum hypothesis ($\mathsf{CH}$) in the Lean theorem prover. We use Boolean-valued models to give forcing arguments for both directions, using Cohen forcing for the consistency of $\neg \mathsf{CH}$ and a $σ$-closed forcing for the consistency of $\mathsf{CH}$.
△ Less
Submitted 4 February, 2021;
originally announced February 2021.
-
Progress on a perimeter surveillance problem
Authors:
Jeremy Avigad,
Floris van Doorn
Abstract:
We consider a perimeter surveillance problem introduced by Kingston, Beard, and Holt in 2008 and studied by Davis, Humphrey, and Kingston in 2019. In this problem, $n$ drones surveil a finite interval, moving at uniform speed and exchanging information only when they meet another drone. Kingston et al. described a particular online algorithm for coordinating their behavior and asked for an upper b…
▽ More
We consider a perimeter surveillance problem introduced by Kingston, Beard, and Holt in 2008 and studied by Davis, Humphrey, and Kingston in 2019. In this problem, $n$ drones surveil a finite interval, moving at uniform speed and exchanging information only when they meet another drone. Kingston et al. described a particular online algorithm for coordinating their behavior and asked for an upper bound on how long it can take before the drones are fully synchronized. They divided the algorithm's behavior into two phases, and presented upper bounds on the length of each phase based on conjectured worst-case configurations. Davis et al. presented counterexamples to the conjecture for phase 1.
We present sharp upper bounds on phase 2 which show that in this case the conjectured worst case is correct. We also present new lower bounds on phase 1 and the total time to synchronization, and report partial progress towards obtaining an upper bound.
△ Less
Submitted 3 June, 2021; v1 submitted 10 August, 2020;
originally announced August 2020.
-
Maintaining a Library of Formal Mathematics
Authors:
Floris van Doorn,
Gabriel Ebner,
Robert Y. Lewis
Abstract:
The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied aud…
▽ More
The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied audience.
△ Less
Submitted 26 May, 2020; v1 submitted 7 April, 2020;
originally announced April 2020.
-
Locally Optimized Random Forests
Authors:
Tim Coleman,
Kimberly Kaufeld,
Mary Frances Dorn,
Lucas Mentch
Abstract:
Standard supervised learning procedures are validated against a test set that is assumed to have come from the same distribution as the training data. However, in many problems, the test data may have come from a different distribution. We consider the case of having many labeled observations from one distribution, $P_1$, and making predictions at unlabeled points that come from $P_2$. We combine…
▽ More
Standard supervised learning procedures are validated against a test set that is assumed to have come from the same distribution as the training data. However, in many problems, the test data may have come from a different distribution. We consider the case of having many labeled observations from one distribution, $P_1$, and making predictions at unlabeled points that come from $P_2$. We combine the high predictive accuracy of random forests (Breiman, 2001) with an importance sampling scheme, where the splits and predictions of the base-trees are done in a weighted manner, which we call Locally Optimized Random Forests. These weights correspond to a non-parametric estimate of the likelihood ratio between the training and test distributions. To estimate these ratios with an unlabeled test set, we make the covariate shift assumption, where the differences in distribution are only a function of the training distributions (Shimodaira, 2000.) This methodology is motivated by the problem of forecasting power outages during hurricanes. The extreme nature of the most devastating hurricanes means that typical validation set ups will overly favor less extreme storms. Our method provides a data-driven means of adapting a machine learning method to deal with extreme events.
△ Less
Submitted 26 August, 2019;
originally announced August 2019.
-
A formalization of forcing and the unprovability of the continuum hypothesis
Authors:
Jesse Michael Han,
Floris van Doorn
Abstract:
We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. As an application of our framework, we specialize our construction to the Boolean algebra of regular opens of the Cantor space $2^{ω_2 \times ω}$ and formally verify the failu…
▽ More
We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. As an application of our framework, we specialize our construction to the Boolean algebra of regular opens of the Cantor space $2^{ω_2 \times ω}$ and formally verify the failure of the continuum hypothesis in the resulting model.
△ Less
Submitted 23 April, 2019;
originally announced April 2019.
-
On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
Authors:
Floris van Doorn
Abstract:
The goal of this dissertation is to present synthetic homotopy theory in the setting of homotopy type theory. We will present various results in this framework, most notably the construction of the Atiyah-Hirzebruch and Serre spectral sequences for cohomology, which have been fully formalized in the Lean proof assistant.
The goal of this dissertation is to present synthetic homotopy theory in the setting of homotopy type theory. We will present various results in this framework, most notably the construction of the Atiyah-Hirzebruch and Serre spectral sequences for cohomology, which have been fully formalized in the Lean proof assistant.
△ Less
Submitted 31 August, 2018;
originally announced August 2018.
-
Beyond Trees: Classification with Sparse Pairwise Dependencies
Authors:
Yaniv Tenzer,
Amit Moscovich,
Mary Frances Dorn,
Boaz Nadler,
Clifford Spiegelman
Abstract:
Several classification methods assume that the underlying distributions follow tree-structured graphical models. Indeed, trees capture statistical dependencies between pairs of variables, which may be crucial to attain low classification errors. The resulting classifier is linear in the log-transformed univariate and bivariate densities that correspond to the tree edges. In practice, however, obse…
▽ More
Several classification methods assume that the underlying distributions follow tree-structured graphical models. Indeed, trees capture statistical dependencies between pairs of variables, which may be crucial to attain low classification errors. The resulting classifier is linear in the log-transformed univariate and bivariate densities that correspond to the tree edges. In practice, however, observed data may not be well approximated by trees. Yet, motivated by the importance of pairwise dependencies for accurate classification, here we propose to approximate the optimal decision boundary by a sparse linear combination of the univariate and bivariate log-transformed densities. Our proposed approach is semi-parametric in nature: we non-parametrically estimate the univariate and bivariate densities, remove pairs of variables that are nearly independent using the Hilbert-Schmidt independence criteria, and finally construct a linear SVM on the retained log-transformed densities. We demonstrate using both synthetic and real data that our resulting classifier, denoted SLB (Sparse Log-Bivariate density), is competitive with popular classification methods.
△ Less
Submitted 16 April, 2020; v1 submitted 5 June, 2018;
originally announced June 2018.
-
Higher Groups in Homotopy Type Theory
Authors:
Ulrik Buchholtz,
Floris van Doorn,
Egbert Rijke
Abstract:
We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups an…
▽ More
We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.
△ Less
Submitted 12 February, 2018;
originally announced February 2018.
-
Homotopy Type Theory in Lean
Authors:
Floris van Doorn,
Jakob von Raumer,
Ulrik Buchholtz
Abstract:
We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of just a few primitive notions of higher inductive types, namely quotients and truncations, and the use of cubical methods.
We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of just a few primitive notions of higher inductive types, namely quotients and truncations, and the use of cubical methods.
△ Less
Submitted 20 September, 2017; v1 submitted 22 April, 2017;
originally announced April 2017.
-
Constructing the Propositional Truncation using Non-recursive HITs
Authors:
Floris van Doorn
Abstract:
In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have f…
▽ More
In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all the results in a new proof assistant, Lean.
△ Less
Submitted 7 December, 2015;
originally announced December 2015.
-
Propositional Calculus in Coq
Authors:
Floris van Doorn
Abstract:
I formalize important theorems about classical propositional logic in the proof assistant Coq. The main theorems I prove are (1) the soundness and completeness of natural deduction calculus, (2) the equivalence between natural deduction calculus, Hilbert systems and sequent calculus and (3) cut elimination for sequent calculus.
I formalize important theorems about classical propositional logic in the proof assistant Coq. The main theorems I prove are (1) the soundness and completeness of natural deduction calculus, (2) the equivalence between natural deduction calculus, Hilbert systems and sequent calculus and (3) cut elimination for sequent calculus.
△ Less
Submitted 31 March, 2015; v1 submitted 30 March, 2015;
originally announced March 2015.
-
Beyond Bidimensionality: Parameterized Subexponential Algorithms on Directed Graphs
Authors:
Frederic Dorn,
Fedor V. Fomin,
Daniel Lokshtanov,
Venkatesh Raman,
Saket Saurabh
Abstract:
We develop two different methods to achieve subexponential time parameterized algorithms for problems on sparse directed graphs. We exemplify our approaches with two well studied problems.
For the first problem, {\sc $k$-Leaf Out-Branching}, which is to find an oriented spanning tree with at least $k$ leaves, we obtain an algorithm solving the problem in time…
▽ More
We develop two different methods to achieve subexponential time parameterized algorithms for problems on sparse directed graphs. We exemplify our approaches with two well studied problems.
For the first problem, {\sc $k$-Leaf Out-Branching}, which is to find an oriented spanning tree with at least $k$ leaves, we obtain an algorithm solving the problem in time $2^{O(\sqrt{k} \log k)} n+ n^{O(1)}$ on directed graphs whose underlying undirected graph excludes some fixed graph $H$ as a minor. For the special case when the input directed graph is planar, the running time can be improved to $2^{O(\sqrt{k})}n + n^{O(1)}$. The second example is a generalization of the {\sc Directed Hamiltonian Path} problem, namely {\sc $k$-Internal Out-Branching}, which is to find an oriented spanning tree with at least $k$ internal vertices. We obtain an algorithm solving the problem in time $2^{O(\sqrt{k} \log k)} + n^{O(1)}$ on directed graphs whose underlying undirected graph excludes some fixed apex graph $H$ as a minor. Finally, we observe that for any $ε>0$, the {\sc $k$-Directed Path} problem is solvable in time $O((1+ε)^k n^{f(ε)})$, where $f$ is some function of $\ve$.
Our methods are based on non-trivial combinations of obstruction theorems for undirected graphs, kernelization, problem specific combinatorial structures and a layering technique similar to the one employed by Baker to obtain PTAS for planar graphs.
△ Less
Submitted 6 January, 2010;
originally announced January 2010.
-
Planar Subgraph Isomorphism Revisited
Authors:
Frederic Dorn
Abstract:
The problem of Subgraph Isomorphism is defined as follows: Given a pattern H and a host graph G on n vertices, does G contain a subgraph that is isomorphic to H? Eppstein [SODA 95, J'GAA 99] gives the first linear time algorithm for subgraph isomorphism for a fixed-size pattern, say of order k, and arbitrary planar host graph, improving upon the O(n^\sqrt{k})-time algorithm when using the ``Colo…
▽ More
The problem of Subgraph Isomorphism is defined as follows: Given a pattern H and a host graph G on n vertices, does G contain a subgraph that is isomorphic to H? Eppstein [SODA 95, J'GAA 99] gives the first linear time algorithm for subgraph isomorphism for a fixed-size pattern, say of order k, and arbitrary planar host graph, improving upon the O(n^\sqrt{k})-time algorithm when using the ``Color-coding'' technique of Alon et al [J'ACM 95]. Eppstein's algorithm runs in time k^O(k) n, that is, the dependency on k is superexponential. We solve an open problem posed in Eppstein's paper and improve the running time to 2^O(k) n, that is, single exponential in k while kee** the term in n linear. Next to deciding subgraph isomorphism, we can construct a solution and enumerate all solutions in the same asymptotic running time. We may list w subgraphs with an additive term O(w k) in the running time of our algorithm. We introduce the technique of "embedded dynamic programming" on a suitably structured graph decomposition, which exploits the topology of the underlying embeddings of the subgraph pattern (rather than of the host graph). To achieve our results, we give an upper bound on the number of partial solutions in each dynamic programming step as a function of pattern size--as it turns out, for the planar subgraph isomorphism problem, that function is single exponential in the number of vertices in the pattern.
△ Less
Submitted 25 September, 2009;
originally announced September 2009.
-
Tight Bounds and Faster Algorithms for Directed Max-Leaf Problems
Authors:
Paul Bonsma,
Frederic Dorn
Abstract:
An out-tree $T$ of a directed graph $D$ is a rooted tree subgraph with all arcs directed outwards from the root. An out-branching is a spanning out-tree. By $l(D)$ and $l_s(D)$ we denote the maximum number of leaves over all out-trees and out-branchings of $D$, respectively.
We give fixed parameter tractable algorithms for deciding whether $l_s(D)\geq k$ and whether $l(D)\geq k$ for a digraph…
▽ More
An out-tree $T$ of a directed graph $D$ is a rooted tree subgraph with all arcs directed outwards from the root. An out-branching is a spanning out-tree. By $l(D)$ and $l_s(D)$ we denote the maximum number of leaves over all out-trees and out-branchings of $D$, respectively.
We give fixed parameter tractable algorithms for deciding whether $l_s(D)\geq k$ and whether $l(D)\geq k$ for a digraph $D$ on $n$ vertices, both with time complexity $2^{O(k\log k)} \cdot n^{O(1)}$. This improves on previous algorithms with complexity $2^{O(k^3\log k)} \cdot n^{O(1)}$ and $2^{O(k\log^2 k)} \cdot n^{O(1)}$, respectively.
To obtain the complexity bound in the case of out-branchings, we prove that when all arcs of $D$ are part of at least one out-branching, $l_s(D)\geq l(D)/3$. The second bound we prove in this paper states that for strongly connected digraphs $D$ with minimum in-degree 3, $l_s(D)\geq Θ(\sqrt{n})$, where previously $l_s(D)\geq Θ(\sqrt[3]{n})$ was the best known bound. This bound is tight, and also holds for the larger class of digraphs with minimum in-degree 3 in which every arc is part of at least one out-branching.
△ Less
Submitted 12 April, 2008;
originally announced April 2008.
-
An FPT Algorithm for Directed Spanning k-Leaf
Authors:
Paul Bonsma,
Frederic Dorn
Abstract:
An out-branching of a directed graph is a rooted spanning tree with all arcs directed outwards from the root. We consider the problem of deciding whether a given directed graph D has an out-branching with at least k leaves (Directed Spanning k-Leaf). We prove that this problem is fixed parameter tractable, when k is chosen as the parameter. Previously this was only known for restricted classes o…
▽ More
An out-branching of a directed graph is a rooted spanning tree with all arcs directed outwards from the root. We consider the problem of deciding whether a given directed graph D has an out-branching with at least k leaves (Directed Spanning k-Leaf). We prove that this problem is fixed parameter tractable, when k is chosen as the parameter. Previously this was only known for restricted classes of directed graphs.
The main new ingredient in our approach is a lemma that shows that given a locally optimal out-branching of a directed graph in which every arc is part of at least one out-branching, either an out-branching with at least k leaves exists, or a path decomposition with width O(k^3) can be found. This enables a dynamic programming based algorithm of running time 2^{O(k^3 \log k)} n^{O(1)}, where n=|V(D)|.
△ Less
Submitted 26 November, 2007;
originally announced November 2007.
