we-solve (beta)

Math-2686 · mathematics · Dynamical systems

Pointwise convergence of fourfold ergodic averages under mixing

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every invertible mixing probability-preserving transformation T and bounded measurable $f_1,f_2,f_3,f_4$, do $(1/N)sum_{n=1}^N$ $f_1(T^n$ $x)f_2(T^{2n}x)f_3(T^{3n}x)f_4(T^{4n}x)$ converge almost everywhere to the product of the four integrals?

Short English statement

For every invertible mixing probability-preserving transformation T and bounded measurable $f_1,f_2,f_3,f_4$, do $(1/N)sum_{n=1}^N$ $f_1(T^n$ $x)f_2(T^{2n}x)f_3(T^{3n}x)f_4(T^{4n}x)$ converge almost everywhere to the product of the four integrals?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2686-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2686

Manuscript 1 (family 154, 2026-10-04): The selected question is contained in the manuscript statement summarized here. Its broader range or additional conclusion therefore gives a claimed proof of the question as a specialization.

Manuscript 2 (family 154, 2026-10-04): The problem selects the mathematical statement summarized here, including its stated hypotheses and parameter range. The cited theorem gives a claimed proof of that assertion in full.

Pointwise convergence of fourfold ergodic averages under mixing

OpenAI's claim

Manuscript 1 (family 154, 2026-10-04): For every invertible mixing transformation, consecutive multiple ergodic averages of any fixed finite length are claimed to have an almost-everywhere limit equal to the product of the input integrals, without a mixing rate. Manuscript 2 (family 154, 2026-10-04): Fourfold averages at times $n,2n,3n,4n$ are claimed to converge pointwise to the product of integrals for every invertible mixing system and bounded inputs on arbitrary probability spaces.

Mathematical statement of the claimed result

Mathematical claim 1.
Let $(X,\mathcal F,\mu)$ be any probability space with an invertible bimeasurable measure-preserving transformation $T$. Assume mixing, meaning $\mu(A\cap T^{-m}B)\to\mu(A)\mu(B)$ as $|m|\to\infty$ for all measurable $A,B$. OpenAI claims, for every $n\ge2$ and every fixed bounded measurable $f_1,\ldots,f_n$, \[ \frac1N\sum_{k=1}^N\prod_{j=1}^n f_j(T^{jk}x)\longrightarrow\prod_{j=1}^n\int_X f_j\,d\mu \quad\text{for almost every }x. \] The limit uses all positive integers $N$, requires no mixing rate or standardness of the probability space, and its null exceptional set may depend on the functions.
Mathematical claim 2.
For any probability space and any invertible bimeasurable measure-preserving mixing $T$, OpenAI claims for every fixed $f_1,\ldots,f_4\in L^\infty(\mu)$ that \[ \frac1N\sum_{k=1}^N\prod_{j=1}^4 f_j(T^{jk}x)\longrightarrow\prod_{j=1}^4\int_X f_j\,d\mu \quad\mu\text{-almost everywhere}. \] Mixing means $\mu(A\cap T^{-m}B)\to\mu(A)\mu(B)$ for every measurable $A,B$ as $|m|\to\infty$; no quantitative rate or standard-space assumption is imposed, and convergence is along all positive $N$.

Outline of the argument

Manuscript 1 (family 154, 2026-10-04): A minimal nonzero centered correlation makes smaller selected spatial lists independent. Conditional-expectation energy saturation stabilizes extensions, and a square joining array is regrouped to create an additional output-only slot; maximality of that slot count gives a contradiction using only the existing at-most-three-slot pointwise theorem.

Manuscript 2 (family 154, 2026-10-04): Three-slot oscillation estimates and the companion multiple-mixing theorem supply the analytic inputs. Selected joining laws are packed into iterated arrays, where orthogonality bounds the number of extra-coordinate slots; saturated conditional laws and reanchoring increase that number, contradicting its maximal choice.

Formal verification

Family 154 has no Lean scope page in this snapshot; no formalization of these manuscript results is listed.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

Go to contribution →