Skip to content

Catalog · 10.5281/zenodo.23451718

Simultaneous avoidance of power families of null sequences

  • Martino Lupini · University of Bologna

18 October 2026 · CC BY 4.0 · latest of 2 versions

MathematicsPDF · LaTeX · Lean · Notes · Data

On the deposit

Simultaneous avoidance of power families of null sequences

Martino Lupini

Abstract

Let (a_n) be a positive sequence tending to zero with liminf a_(n+1)/a_n > 0. For every η ∈ (0,1), we construct a compact set E ⊆ [0,1] of Lebesgue measure greater than 1−η such that {x+s a_n^λ : n ≥ 1} is not contained in E for any x ∈ ℝ, s ≠ 0, and λ > 0. No monotonicity is required, and one set works for all positive powers simultaneously, with infinitely many distinct points of every copy outside E. Taking a_n=e^(−n) gives one compact set of measure arbitrarily close to one containing no infinite geometric progression of any ratio in (0,1), answering negatively a question of Burgin, Goldberg, Keleti, MacMahon and Wang. We also prove a uniform finite hitting statement for ratios in a compact range and scales in [1,2]. The proof adapts random routing to grids shared by all exponents, with a localized count of exponent and scale parameters and a compactness repair for exceptional centres.

GitHub repository: https://github.com/eulogica/power-family-avoidance

10.5281/zenodo.23451718

Files

What this version of the record actually contains. Text sources can be read here. PDFs and archives open on Zenodo. Zenodo does not allow the PDF to be framed on another site.

  • lake-manifest.json

    JSON · 150 B

  • lean-toolchain

    File · 26 B

  • simultaneous-geometric-avoidance.pdf

    PDF · 486.7 KB

    Open on Zenodo
  • lakefile.lean

    Lean · 126 B

  • verification-output.txt

    Notes · 2.6 KB

  • simultaneous-geometric-avoidance.tex

    LaTeX · 74.0 KB

  • PowerFamilies.lean

    Lean · 6.9 KB

  • Audit.lean

    Lean · 955 B

  • verification.md

    Notes · 7.3 KB

  • proof-ledger.md

    Notes · 9.0 KB

  • LEAN-SUPPLEMENT.txt

    Notes · 1.7 KB

  • formalization-map.md

    Notes · 10.8 KB

Other homes

Zenodo

The deposit of record for this version.

GitHub

Named in the manuscript. This page does not check whether the repository is public.

Obsidian

Not recorded on this deposit.

BibTeX

@unpublished{Lupini202623451718,
  title = {Simultaneous avoidance of power families of null sequences},
  author = {Martino Lupini},
  year = {2026},
  doi = {10.5281/zenodo.23451718},
  note = {Zenodo deposit, latest of 2}
}