These files accompany a formalization of the main results of the paper Estimation Error in Latent High-Dimensional Factor Models (estimation-error.pdf). This is built using Lean 4.28.0 with mathlib 4.28.0. Compilation with earlier or later versions are not guaranteed due to the quick-changing nature of Lean and mathlib.
The formalization establishes Theorem 1 and Corollaries 1–3 of the paper, assuming three classical background facts that are not yet available in Mathlib:
- The Kolmogorov strong law of large numbers for independent, non-identically distributed summands
- Weyl's eigenvalue perturbation inequality
- Eigenvector continuity for a simple eigenvalue (Davis–Kahan).
- Input:
- estimation-error.pdf: The source paper, whose Theorem 1 and Corollaries 1–3 are the targets of the formalization.
- assumed-facts.tex: The three classical background facts assumed by the formalization (Kolmogorov SLLN, Weyl's inequality, Davis–Kahan eigenvector continuity), each stated exactly as it appears as a hypothesis in Lean.
- task.md: The formalization instructions.
- Output:
- problem.lean: An autonomously generated formal statement of the task.
- solution.lean: An autonomously generated formal proof of the task, matching
problem.lean.