Added some \lean's and \leanok's to the blueprint, split proofs in 10.2 and 11.6.

Carleson.lean

@@ -12,15 +12,15 @@ import Carleson.HolderVanDerCorput
 import Carleson.MetricCarleson
 import Carleson.Psi
 import Carleson.RealInterpolation
-import Carleson.Theorem1_1.Approximation
-import Carleson.Theorem1_1.Basic
-import Carleson.Theorem1_1.CarlesonOperatorReal
-import Carleson.Theorem1_1.Carleson_on_the_real_line
-import Carleson.Theorem1_1.ClassicalCarleson
-import Carleson.Theorem1_1.Control_Approximation_Effect
-import Carleson.Theorem1_1.Dirichlet_kernel
-import Carleson.Theorem1_1.Hilbert_kernel
-import Carleson.Theorem1_1.Van_der_Corput
+import Carleson.Classical.Approximation
+import Carleson.Classical.Basic
+import Carleson.Classical.CarlesonOperatorReal
+import Carleson.Classical.CarlesonOnTheRealLine
+import Carleson.Classical.ClassicalCarleson
+import Carleson.Classical.ControlApproximationEffect
+import Carleson.Classical.DirichletKernel
+import Carleson.Classical.HilbertKernel
+import Carleson.Classical.SpectralProjectionBound
 import Carleson.TileExistence
 import Carleson.TileStructure
 import Carleson.ToMathlib.Finiteness

Carleson/Theorem1_1/Approximation.lean → Carleson/Classical/Approximation.lean

@@ -1,7 +1,7 @@
 /- The arguments in this file replace section 10.2 (Piecewise constant functions) from the paper. -/
 
 import Carleson.MetricCarleson
-import Carleson.Theorem1_1.Basic
+import Carleson.Classical.Basic
 
 import Mathlib.Analysis.Fourier.AddCircle
 import Mathlib.Analysis.Convolution
@@ -32,7 +32,8 @@ lemma uniformContinuous_iff_bounded [PseudoMetricSpace α] [PseudoMetricSpace β
 end section
 
 /- TODO: might be generalized. -/
-lemma closeSmoothApprox {f : ℝ → ℂ} (unicontf : UniformContinuous f) {ε : ℝ} (εpos : ε > 0):
+--TODO: probably not needed here in this form
+lemma close_smooth_approx {f : ℝ → ℂ} (unicontf : UniformContinuous f) {ε : ℝ} (εpos : ε > 0):
     ∃ (f₀ : ℝ → ℂ), ContDiff ℝ ⊤ f₀ ∧ ∀ x, Complex.abs (f x - f₀ x) ≤ ε := by
   obtain ⟨δ, δpos, hδ⟩ := (Metric.uniformContinuous_iff.mp unicontf) ε εpos
   let φ : ContDiffBump (0 : ℝ) := ⟨δ/2, δ, by linarith, by linarith⟩
@@ -46,7 +47,7 @@ lemma closeSmoothApprox {f : ℝ → ℂ} (unicontf : UniformContinuous f) {ε :
       fun y hy ↦ (hδ hy).le
 
 /- Slightly different version-/
-lemma closeSmoothApproxPeriodic {f : ℝ → ℂ} (unicontf : UniformContinuous f)
+lemma close_smooth_approx_periodic {f : ℝ → ℂ} (unicontf : UniformContinuous f)
   (periodicf : f.Periodic (2 * Real.pi)) {ε : ℝ} (εpos : ε > 0):
     ∃ (f₀ : ℝ → ℂ), ContDiff ℝ ⊤ f₀ ∧ f₀.Periodic (2 * Real.pi) ∧
       ∀ x, Complex.abs (f x - f₀ x) ≤ ε := by

Carleson/Theorem1_1/Basic.lean → Carleson/Classical/Basic.lean

@@ -12,6 +12,11 @@ noncomputable section
 --TODO : add reasonable notation
 --local notation "S_" => partialFourierSum f
 
+--TODO: use this as base to build on?
+def AddCircle.partialFourierSum' {T : ℝ} [hT : Fact (0 < T)] (f : AddCircle T → ℂ) (N : ℕ) (x : AddCircle T) : ℂ :=
+    ∑ n in Icc (-Int.ofNat ↑N) N, fourierCoeff f n * fourier n x
+
+--TODO: switch N and f
 def partialFourierSum (f : ℝ → ℂ) (N : ℕ) : ℝ → ℂ := fun x ↦ ∑ n in Icc (-Int.ofNat ↑N) N, fourierCoeffOn Real.two_pi_pos f n * fourier n (x : AddCircle (2 * Real.pi))
 --fun x ↦ ∑ n in Icc (-Int.ofNat ↑N) N, fourierCoeffOn Real.two_pi_pos f n * fourier n (x : AddCircle (2 * Real.pi))
 
@@ -76,8 +81,6 @@ theorem Function.Periodic.exists_mem_Ico₀' {α : Type} {β : Type} {f : α →
 
 --TODO: maybe generalize to (hc : ContinuousOn f (Set.Icc 0 T)) and leave out condition (hT : 0 < T)
 lemma Function.Periodic.uniformContinuous_of_continuous {f : ℝ → ℂ} {T : ℝ} (hT : 0 < T) (hp : Function.Periodic f T) (hc : ContinuousOn f (Set.Icc (-T) (2 * T))) : UniformContinuous f := by
-  --rw [Metric.uniformContinuous_iff]
-  --IsCompact.uniformContinuous_on
   have : IsCompact (Set.Icc (-T) (2 * T)) := isCompact_Icc
   have unicont_on_Icc := this.uniformContinuousOn_of_continuous hc
   rw [Metric.uniformContinuousOn_iff] at unicont_on_Icc
@@ -114,7 +117,6 @@ theorem strictConvexOn_cos_Icc : StrictConvexOn ℝ (Set.Icc (Real.pi / 2) (Real
   rw [interior_Icc] at hx
   simp [Real.cos_neg_of_pi_div_two_lt_of_lt hx.1 hx.2]
 
-/- Lemma 10.11 (lower secant bound) from the paper. -/
 lemma lower_secant_bound' {η : ℝ}  {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_le : |x| ≤ 2 * Real.pi - η) :
     (2 / Real.pi) * η ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by
   by_cases ηpos : η ≤ 0
@@ -208,15 +210,3 @@ lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * Real.p
     apply lower_secant_bound' xAbs
     rw [abs_le, neg_sub', sub_neg_eq_add, neg_mul_eq_neg_mul]
     exact xIcc
-
-/-Further definitions-/
-/-TODO : relocate this-/
-
---TODO : call constructor in a better way?
-def integer_linear (n : ℤ) : C(ℝ, ℝ) := ⟨fun (x : ℝ) ↦ n * x, by fun_prop⟩
-
---local notation "θ" => integer_linear
-
---lemma θcont {n : ℤ} : Continuous (θ n) := sorry
-
---local notation "Θ" => {(θ n) | n : ℤ}