google-deepmind / google-deepmind/formal-conjectures

Erdős Problem 671

Open
#869 0 comments 0 reactions 0 assignees View on GitHub
ams-12: Field theory and polynomials ams-26: Real functions erdos-problems new conjecture
Dominant language
Lean
Stars
1.3k
Forks
485
Avg merge
1d 20h
Merged PRs (30d)
328

Description

### What is the conjecture

https://www.erdosproblems.com/671

Given $a_{i}^n\in [-1,1]$ for all $1\leq i\leq n<\infty$ we define $p_{i}^n$ as the unique polynomial of degree $n-1$ such that $p_{i}^n(a_{i}^n)=1$ and $p_{i}^n(a_{i'}^n)=0$ if $1\leq i'\leq n$ with $i\neq i'$. We similarly define
$$\mathcal{L}^nf(x) = \sum_{1\leq i\leq n}f(a_i^n)p_i^n(x),$$
the unique polynomial of degree $n-1$ which agrees with $f$ on $a_i^n$ for $1\leq i\leq n$ (that is, the sequence of Langrange interpolation polynomials).

Is there such a sequence of $a_i^n$ such that for every continuous $f:[-1,1]\to \mathbb{R}$ there exists some $x\in [-1,1]$ where
$$\limsup_{n\to \infty} \sum_{1\leq i\leq n}\lvert p_{i}^n(x)\rvert=\infty$$
and yet
$$\mathcal{L}^nf(x) \to f(x)?$$

Is there such a sequence such that

$$\limsup_{n\to \infty} \sum_{1\leq i\leq n}\lvert p_{i}^n(x)\rvert=\infty$$
for every $x\in [-1,1]$ and yet for every continuous $f:[-1,1]\to \mathbb{R}$ there exists $x\in [-1,1]$ with
$$\mathcal{L}^nf(x) \to f(x)?$$

Status: open

### Choose either option
- [ ] I plan on working on this conjecture
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.