Erdős Problem 1153: Lagrange Basis Polynomial Sum Bound on Subintervals

### What is the conjecture

For points $x_1, \ldots, x_n \in [-1,1]$, define the Lagrange basis polynomials $$l_k(x)=\frac{\prod_{i\neq k}(x-x_i)}{\prod_{i\neq k}(x_k-x_i)}$$ Let $\lambda(x)=\sum_{k=1}^{n} |l_k(x)|$ be the sum of absolute values of the Lagrange basis polynomials (known as the Lebesgue constant). For any fixed interval $[a, b] \subseteq [-1, 1]$, does there exist a sequence of points $x_1, \ldots, x_n$ in $[-1,1]$ such that $$\max_{x\in [a,b]}\lambda(x) > \left(\frac{2}{\pi}-o(1)\right)\log n$$ This is an open problem asking whether the logarithmic lower bound holds uniformly for all subintervals, not just the full interval $[-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/1153

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Polynomial type and evaluation in Mathlib (standard `Polynomial` type)
- Real-valued functions and absolute value operations
- Asymptotic notation and $o(n)$ definition

Missing pieces (exactly 2; unclear/absent from search results):
- Formalization of Lagrange interpolation and the basis polynomials as defined
- Formal definition of the Lebesgue constant and its asymptotic properties

Rating justification (1-2 sentences): The core mathematical objects (polynomials, real functions, absolute values) are well-established in Mathlib, so the statement can be written using existing types. However, the specific definition of Lagrange basis polynomials and Lebesgue constants will require some auxiliary definitions to express cleanly, making this a 2-rated formalization target.

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

* ams-41
* ams-12

### 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)