Erdős Problem 996

Reference:

• erdosproblems.com/996
• [Er49d] Erdös, P. "On the strong law of large numbers." Transactions of the American Mathematical Society 67.1 (1949): 51-56.
• [Ma66] Matsuyama, Noboru. "On the strong law of large numbers." Tohoku Mathematical Journal, Second Series 18.3 (1966): 259-269.

noncomputable def fourierPartial {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (k : ℕ) : AddCircle T → ℂ

Equations

• fourierPartial f k x = ∑ i ∈ Finset.Icc (-↑k) ↑k, fourierCoeff ↑↑f ↑k • (fourier i) x

theorem Erdos996.erdos_996.log3 : sorry ↔ ∃ (C : ℝ), 0 < C ∧ ∀ (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (n : ℕ → ℕ), IsLacunary n → ((fun (k : ℕ) => (MeasureTheory.eLpNorm (fourierPartial f k) 2 AddCircle.haarAddCircle).toReal) =O[Filter.atTop] fun (k : ℕ) => 1 / Real.log (Real.log (Real.log ↑k)) ^ C) → ∀ᵐ (x : AddCircle 1), Filter.Tendsto (fun (N : ℕ) => (∑ k ∈ Finset.range N, ↑↑f (n k • x)) / ↑N) Filter.atTop (nhds (∫ (t : AddCircle 1), ↑↑f t ∂AddCircle.haarAddCircle))

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?

theorem Erdos996.erdos_996.log2 (C : ℝ) : 0.5 < C → ∀ (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (n : ℕ → ℕ), IsLacunary n → ((fun (k : ℕ) => (MeasureTheory.eLpNorm (fourierPartial f k) 2 AddCircle.haarAddCircle).toReal) =O[Filter.atTop] fun (k : ℕ) => 1 / Real.log (Real.log ↑k) ^ C) → ∀ᵐ (x : AddCircle 1), Filter.Tendsto (fun (N : ℕ) => (∑ k ∈ Finset.range N, ↑↑f (n k • x)) / ↑N) Filter.atTop (nhds (∫ (t : AddCircle 1), ↑↑f t ∂AddCircle.haarAddCircle))

The following theorem is proved in [Ma66].