Erdős ProblemsHarmonic analysis
Erdős Problem 996
Does there exists a positive constant C such that for all f ∈ L²[0,1] and all lacunary sequences n, if ‖f - fₖ‖₂ = O(1 / log log log k ^ C), then for almost every x, lim ∑ k ∈ Finset.range N, f (n k • x)) / N = ∫ t, f t ∂t?
Mathematical statement
Does there exists a positive constant C such that for all f ∈ L²[0,1] and all lacunary
sequences n, if ‖f - fₖ‖₂ = O(1 / log log log k ^ C), then for almost every x,
lim ∑ k ∈ Finset.range N, f (n k • x)) / N = ∫ t, f t ∂t?
Statement source: Erdős Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
erdos_996
theorem erdos_996 : answer(sorry) ↔ ∃ (C : ℝ), 0 < C ∧ ∀ (f : Lp ℂ 2 (haarAddCircle (T := 1))) (n : ℕ → ℕ), IsLacunary n → (fun k => (eLpNorm (fourierPartial f k) 2 (haarAddCircle (T := 1))).toReal) =O[atTop] (fun k => 1 / (log (log (log k))) ^ C) → ∀ᵐ x, Tendsto (fun N => (∑ k ∈ .range N, f (n k • x)) / N) atTop (𝓝 (∫ t, f t ∂haarAddCircle)) := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References