From 55653f7add3f01550a5993a6f529ec84c85a2b82 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Fri, 19 Apr 2024 09:42:43 +0200
Subject: [PATCH] remove classical file

---
 Carleson/Classical.lean | 30 ------------------------------
 1 file changed, 30 deletions(-)
 delete mode 100644 Carleson/Classical.lean

diff --git a/Carleson/Classical.lean b/Carleson/Classical.lean
deleted file mode 100644
index 41eba024..00000000
--- a/Carleson/Classical.lean
+++ /dev/null
@@ -1,30 +0,0 @@
-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