RandomVarSPR

This repository contains a Lean 4/Mathlib autoformalization of the main result from the preprint Stable Phase Retrieval for Spans of Independent Random Variables, by Pedro Abdalla, Jaume de Dios Pont, João P. G. Ramos, and Mitchell A. Taylor.

A Lean file corresponding to the main result as discussed in Section 6 of the preprint can be found in Showcase.lean. It contains the stable phase retrieval theorem for linear combinations of independent real random variables in L².

The main Lean proof is contained in the QuantitativePR/ folder, organized as follows:

• Core/: finite coefficient models and random variable norms.
• Imported/: reusable probability, L², symmetrization, and combinatorial estimates.
• Head/: the head (concentrated case) estimates.
• Tail/: the tail (diffuse case) estimates.
• OneD/: one-dimensional anticoncentration estimates for random variables.
• Main/: assembly of the result.
• Comparator/: standalone challenge file, solution wrapper, and comparator configuration.

The QuantitativePR_Blueprint/ folder contains a machine-generated blueprint used during the formalization process.

Build

From the repository root, use Lake:

lake build QuantitativePR
lake build Showcase
lake build

The default targets in lakefile.toml are QuantitativePR and Showcase.

Comparator Checks

The repository includes a comparator setup for the public theorem track:

• QuantitativePR/Comparator/config.json

The challenge file imports only Mathlib and restates the public theorem type.

Run the comparator check with:

./scripts/run_local_comparator.sh

If the comparator tools are not installed locally, first run:

./scripts/setup_local_comparator_linux.sh

See Comparator.md for a short note on the comparator setup.