From edbb64e89dfa35ede33c64e676964450f0df3aac Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 17 Apr 2024 18:03:09 +0200
Subject: [PATCH] classical version

---
 Carleson/Classical.lean | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 Carleson/Classical.lean

diff --git a/Carleson/Classical.lean b/Carleson/Classical.lean
new file mode 100644
index 00000000..41eba024
--- /dev/null
+++ b/Carleson/Classical.lean
@@ -0,0 +1,30 @@
+import Carleson.Carleson
+import Mathlib.Analysis.Fourier.AddCircle
+
+/-! The classical version of Carleson's theorem.
+
+For this we take `X = ℝ`, `K x y := 1 / (x - y)` and `Θ = {linear functions}`.
+-/
+
+open MeasureTheory Measure NNReal Metric Complex Set TileStructure Function BigOperators Filter
+open AddCircle Topology
+open scoped ENNReal
+noncomputable section
+
+variable {T : ℝ} {f : AddCircle T → ℂ} {ε : ℝ} [Fact (0 < T)]
+
+
+def partialFourierSum (f : AddCircle T → ℂ) (n : ℤ) (x : AddCircle T) : ℂ :=
+  ∑ i in Finset.Icc (- n) n, fourierCoeff f i * fourier i x
+
+theorem classical_carleson (hf : UniformContinuous f) (h2f : ∀ x, ‖f x‖ ≤ 1)
+    (hε : 0 < ε) :
+    ∃ (E : Set (AddCircle T)) (N₀ : ℕ), MeasurableSet E ∧ haarAddCircle E ≤ .ofReal ε ∧
+    ∀ N x, N₀ ≤ N → x ∉ E → ‖f x - partialFourierSum f N x‖ < ε := by
+  sorry
+
+
+theorem classical_carleson_pointwise (hf : UniformContinuous f) (h2f : ∀ x, ‖f x‖ ≤ 1) :
+    ∃ (E : Set (AddCircle T)) (N₀ : ℕ), MeasurableSet E ∧ haarAddCircle E = 0 ∧
+    ∀ x, x ∉ E → Tendsto (partialFourierSum f · x) atTop (𝓝 (f x)) := by
+  sorry