Erdős Problem 1132 Lagrange Basis Polynomial

### What is the conjecture

Let $x_1, x_2, \ldots, x_n$ be distinct points in $[-1,1]$. The Lagrange basis polynomials are defined by $$l_k(x) = \prod_{j=1, j \neq k}^{n} \frac{x - x_j}{x_k - x_j}$$ Define $$L_n(x) = \sum_{k=1}^{n} |l_k(x)|$$

The problem poses two related questions:
1. Must there exist a point $x \in (-1,1)$ such that $L_n(x) > \frac{2}{\pi}\log n - O(1)$ for infinitely many $n$?
2. Is it true that $\limsup_{n\to \infty}\frac{L_n(x)}{\log n} \geq \frac{2}{\pi}$ for almost all $x \in (-1,1)$?

It is known (Erdős) that $\max_{x \in [-1,1]} L_n(x) > \frac{2}{\pi}\log n - O(1)$, and (Bernstein) that the set of points satisfying the lim sup condition is dense in $(-1,1)$.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://www.erdosproblems.com/1132

### Prerequisites needed

**Formalizability Rating:** 3/5 (0 is best) (as of 2026-02-01)

Building blocks (1-3; from search results):
- Polynomial types and operations in Mathlib (definitions in `Polynomial`)
- Measurability and measure theory basics for "almost all $x$" statements
- Real analysis fundamentals (lim sup, logarithms)

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of Lagrange interpolation basis polynomials and their properties (not standard in Mathlib)
- Infrastructure for stating growth rate properties of sums of absolute values of polynomials

Rating justification: The basic mathematical objects (polynomials, limits, measure) exist in Mathlib, but the specific notion of Lagrange basis polynomials and the property being quantified require moderate new definitions to properly state in Lean.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-41
* ams-26

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)