arXiv subjects

Tanja Schindler

Publications and source records attributed to Tanja Schindler.

13 recordsLinked to original sources

arXiv2026

Dynamical spectrum of power-free integers in quadratic number fields and beyond

Power-free integers and related lattice subsets give rise to interesting dynamical systems. They are revisited from a spectral perspective, in the setting of the Halmos--von Neumann theorem. With respect to the natural patch frequency measure, also known as the Mirsky measure, many of these systems have pure-point dynamical spectrum, but trivial topological point spectrum. We calculate the spectra explicitly, in additive notation, and derive their group structure, both for a large class of $\cB$-free lattice systems in $\RR^d$ and for power-free integers in quadratic number fields. Further, in all cases, the eigenfunctions can be given in closed form, via the Fourier--Bohr coefficients of generic elements and their translates, which form a subset of full Mirsky measure. Based on a simple argument via Kolmogorov's strong law of large numbers, we show how the Fourier--Bohr coefficients also provide the eigenfunctions for the unique measure of maximal entropy, and that we get phase consistency for both measures.

math.DS↗

arXiv2025

Pseudo-Boolean Proof Logging for Optimal Classical Planning

We introduce lower-bound certificates for classical planning tasks, which can be used to prove the unsolvability of a task or the optimality of a plan in a way that can be verified by an independent third party. We describe a general framework for generating lower-bound certificates based on pseudo-Boolean constraints, which is agnostic to the planning algorithm used. As a case study, we show how to modify the $A^{*}$ algorithm to produce proofs of optimality with modest overhead, using pattern database heuristics and $h^\textit{max}$ as concrete examples. The same proof logging approach works for any heuristic whose inferences can be efficiently expressed as reasoning over pseudo-Boolean constraints.

cs.AI↗

arXiv2023

Choose your Colour: Tree Interpolation for Quantified Formulas in SMT

We present a generic tree-interpolation algorithm in the SMT context with quantifiers. The algorithm takes a proof of unsatisfiability using resolution and quantifier instantiation and computes interpolants (which may contain quantifiers). Arbitrary SMT theories are supported, as long as each theory itself supports tree interpolation for its lemmas. In particular, we show this for the theory combination of equality with uninterpreted functions and linear arithmetic. The interpolants can be tweaked by virtually assigning each literal in the proof to interpolation partitions (colouring the literals) in arbitrary ways. The algorithm is implemented in SMTInterpol.

cs.LO↗

arXiv2019

Strong laws of large number for intermediately trimmed Birkhoff sums of observables with infinite mean

We consider dynamical systems on a finite measure space fulfilling a spectral gap property and Birkhoff sums of a non-negative, non-integrable observable. For such systems we generalize strong laws of large numbers for intermediately trimmed sums only known for independent random variables. The results split up in trimming statements for general distribution functions and for regularly varying tail distributions. In both cases the trimming rate can be chosen in the same or almost the same way as in the i.i.d. case. As an example we show that piecewise expanding interval maps fulfill the necessary conditions for our limit laws. As a side result we obtain strong laws of large numbers for truncated Birkhoff sums.

math.DS↗

arXiv2019

Interpolation and the Array Property Fragment

Interpolation based software model checkers have been successfully employed to automatically prove programs correct. Their power comes from interpolating SMT solvers that check the feasibility of potential counterexamples and compute candidate invariants, otherwise. This approach works well for quantifier-free theories, like equality theory or linear arithmetic. For quantified formulas, there are SMT solvers that can decide expressive fragments of quantified formulas, e. g., EPR, the array property fragment, and the finite almost uninterpreted fragment. However, these solvers do not support interpolation. It is already known that in general EPR does not allow for interpolation. In this paper, we show the same result for the array property fragment.

cs.LO↗

arXiv2019

Scaling properties of the Thue--Morse measure

The classic Thue--Morse measure is a paradigmatic example of a purely singular continuous probability measure on the unit interval. Since it has a representation as an infinite Riesz product, many aspects of this measure have been studied in the past, including various scaling properties and a partly heuristic multifractal analysis. Some of the difficulties emerge from the appearance of an unbounded potential in the thermodynamic formalism. It is the purpose of this article to review and prove some of the observations that were previously established via numerical or scaling arguments.

math.DS↗

arXiv2019

Mean convergence for intermediately trimmed Birkhoff sums of observables with regularly varying tails

On a measure theoretical dynamical system with spectral gap property we consider non-integrable observables with regularly varying tails and fulfilling a mild mixing condition. We show that the normed trimmed sum process of these observables then converges in mean. This result is new also for the special case of i.i.d. random variables and contrasts the general case where mean convergence might fail even though a strong law of large numbers holds. To illuminate the required mixing condition we give an explicit example of a dynamical system fulfilling a spectral gap property and an observable with regularly varying tails but without the assumed mixing condition such that mean convergence fails.

math.DS↗

arXiv2019

Intermediately trimmed strong laws for Birkhoff sums on subshifts of finite type

We prove strong laws of large numbers under intermediate trimming for Birkhoff sums over subshifts of finite type. This gives another application of a previous trimming result only proven for interval maps. In case of Markov measures we give a further example of St.\ Petersburg type distribution functions. To prove these statements we introduce the space of quasi-Hölder continuous functions for subshifts of finite type.

math.DS↗

arXiv2018

Limit theorems for counting large continued fraction digits

We establish a central limit theorem for counting large continued fraction digits $(a_n)$, i.e. we count occurrences $\{a_n>b_n\}$, where $(b_n)$ is a sequence of positive integers. Our result improves a similar result by Philipp which additionally assumes that $b_n$ tends to infinity. Moreover, we give a refinement of the famous Borel-Bernstein Theorem for continued fractions regarding the event that the $n$-th continued fraction digit lies infinitely often between $d_n$ and $d_n(1+1/c_n)$ for given sequences $(c_n)$ and $(d_n)$. Also for these sets we obtain a central limit theorem. As an interesting side result we determine the first $ϕ$-mixing coefficient for the Gauss system explicitly.

math.PR↗

arXiv2018

Trimmed sums for observables on the doubling map

We establish a strong law of large numbers under intermediate trimming for a particular example of Birkhoff sums of a non-integrable observable over the doubling map. It has been shown in a previous work by Haynes that there is no strong law of large numbers for the considered system after removing finitely many summands (light trimming) even though i.i.d. random variables and also some dynamical systems with the same distribution function obey a strong law of large numbers after removing only the largest summand.

math.DS↗

arXiv2018

Efficient Interpolation for the Theory of Arrays

Existing techniques for Craig interpolation for the quantifier-free fragment of the theory of arrays are inefficient for computing sequence and tree interpolants: the solver needs to run for every partitioning $(A, B)$ of the interpolation problem to avoid creating $AB$-mixed terms. We present a new approach using Proof Tree Preserving Interpolation and an array solver based on Weak Equivalence on Arrays. We give an interpolation algorithm for the lemmas produced by the array solver. The computed interpolants have worst-case exponential size for extensionality lemmas and worst-case quadratic size otherwise. We show that these bounds are strict in the sense that there are lemmas with no smaller interpolants. We implemented the algorithm and show that the produced interpolants are useful to prove memory safety for C programs.

cs.LO↗

arXiv2018

Small Time Convergence of Subordinators with Regularly or Slowly Varying Canonical Measure

We consider subordinators $X_α=(X_α(t))_{t\ge 0}$ in the domain of attraction at 0 of a stable subordinator $(S_α(t))_{t\ge 0}$ (where $α\in(0,1)$); thus, with the property that $\overlineΠ_α$, the tail function of the canonical measure of $X_α$, is regularly varying of index $-α\in (-1,0)$ as $x\downarrow 0$. We also analyse the boundary case, $α=0$, when $\overlineΠ_α$ is slowly varying at 0. When $α\in(0,1)$, we show that $(t \overlineΠ_α(X_α(t)))^{-1}$ converges in distribution, as $t\downarrow 0$, to the random variable $(S_α(1))^α$. This latter random variable, as a function of $α$, converges in distribution as $α\downarrow 0$ to the inverse of an exponential random variable. We prove these convergences, also generalised to functional versions (convergence in $\mathbb{D}[0,1]$), and to trimmed versions, whereby a fixed number of its largest jumps up to a specified time are subtracted from a process. The $α=0$ case produces convergence to an extremal process constructed from ordered jumps of a Cauchy subordinator. Our results generalise random walk and stable process results of Darling, Cressie, Kasahara, Kotani and Watanabe.

math.PR↗

arXiv2017

Strong laws of large numbers for intermediately trimmed sums of i.i.d. random variables with infinite mean

We consider moderately trimmed sums of non-negative i.i.d. random variables. We show that for every distribution function there exists a proper moderate trimming such that for the trimmed sum a non-trivial strong law of large numbers holds. In case that the distribution function has regularly varying tails we give necessary and sufficient conditions on the trimming for a strong law of large numbers to hold.

math.PR↗