Add files for Classical Carleson (#18)

* Initial experiments and formulation of the Classical Carleson Theorem

* Small improvement

* Formulated some more definitions and lemmas in context, a bit messy however.

* Reduced main theorem to lemmas, modulo some left sorry's

* Added missing last calc step

* State after meeting with recommendations

* Changed back to volume.real in all places; filled in some gaps; minor corrections

* Proved that δ can be chosen less than π and moved this statement to a new lemma

* Stated lemma 10.4

* Created first outline of the proof of Lemma 10.4, i.e. of section 10.7

* Worked on section 10.7; problem occured with Finset in ballsCoverBalls

* Proved lemma 10.37 (Hilbert kernel bound)

* Continued work on section 10.7 and moved this part to a separate file.

* Correct statement and proof of lemma Hilbert kernel bound.

* Minor changes

* Added and proved some lemmas needed for fourierConv_ofTwiceDifferentiable

* Almost done with the top level approximation argument.

* Added and proved lemma about periodicity of deriv.

* Proved lemma int_sum_nat. Simpler parts of approximation argument done.

* Split the main file, part 1.

* Split main file, part 2.

* Added basic facts about partialFourierSum.

* Finished proof of Classical Carleson module Lemma 10.3

* Reshuffling sections

* Proved lemma 10.11 (lower secant bound)

* Did much of the proof of lemma 10.14 (Hilbert kernel regularity).

* Proved Hilbert_kernel_regularity (almost)

* Reshuffled and added some definitions

* Various minor improvements

* Proved Lemma 10.10 (Dirichlet Kernel)

* Proved helper lemma for control_approximation_effect

* Progress on many different parts of control_approximation_effect

* Mathlib update and further work on control_approximation_effect

* open Complex in Control_Approximation_Effect

* More sorry's in Control_Approximation_Effect

* Cleanup of Carleson_on_the_real_line, part 1

* Cleanup Carleson_on_the_real_line part 2

* Cleanup, proved some minor lemmas

* small improvements of control_approximation_effect; no change to ENNReal yet

* Minor exploration of ideas but still stuck.

* Minor additions in Basic

* Added dirichlet_Hilbert_eq lemma

* le_CarlesonOperatorReal' shoud be mostly working now

* Reorganized proof of control_approximation_effect'

* Rewrote proof of control_approximation_effect for ENNReal

* Slightly generalized rcarleson' and other minor changes

* Improved a proof

* Filled in sorry's in Control_Approximation_Effect

* Further cleanup of Control_Approximation_Effect

* Updated classical_carleson to current version of control_approximation_effect

* Further Cleanup of Control_Approximation_Effect

* Control_Approximation_Effect finally sorry-free :)

* Cleanup CarlesonOperatorReal

Carleson.lean

@@ -1 +1,16 @@
-import Carleson.Carleson
+import Carleson.CoverByBalls
+import Carleson.Defs
+import Carleson.HomogeneousType
+import Carleson.Proposition1
+import Carleson.Proposition2
+import Carleson.Proposition3
+import Carleson.Theorem1_1.Approximation
+import Carleson.Theorem1_1.Basic
+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.ToMathlib.Finiteness
+import Carleson.ToMathlib.Finiteness.Attr
+import Carleson.ToMathlib.MeasureReal
+import Carleson.ToMathlib.Misc

Carleson/Carleson.lean

@@ -1,13 +1,20 @@
 import Carleson.Proposition1
+import Mathlib.Tactic.Positivity.Basic
 
 open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators
 open scoped ENNReal
 noncomputable section
 
 /- The constant used in theorem1_2 -/
-def C1_2 (a q : ℝ) : ℝ := 2 ^ (270 * a ^ 3) / (q - 1) ^ 5
+def C1_2 (a q : ℝ) : ℝ := 2 ^ (450 * a ^ 3) / (q - 1) ^ 5
 
-lemma C1_1_pos (a q : ℝ) (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) : C1_2 a q > 0 := sorry
+lemma C1_2_pos {a q : ℝ} (hq : 1 < q) : 0 < C1_2 a q := by
+  rw [C1_2]
+  apply div_pos
+  . apply Real.rpow_pos_of_pos
+    norm_num
+  . apply pow_pos
+    linarith [hq]
 
 /- The constant used in equation (2.2) -/
 def Ce2_2 (A : ℝ) (τ q : ℝ) : ℝ := sorry
@@ -191,5 +198,16 @@ theorem theorem1_2C
     C1_2 a q * (volume.real G) ^ q'⁻¹ * (volume.real F) ^ q⁻¹ := by
   sorry
 
+/- ENNReal version of Theorem 1.2 -/
+--TODO: Change definition of ANCZOperator and ANCZOperatorLp as well?
+theorem theorem1_2C'
+    (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q')
+    (hF : MeasurableSet F) (hG : MeasurableSet G)
+    -- (h2F : volume F ∈ Ioo 0 ∞) (h2G : volume G ∈ Ioo 0 ∞)
+    (hT : NormBoundedBy (ANCZOperatorLp 2 K) 1) (f : X → ℂ)
+    (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
+    ∫⁻ x in G, CarlesonOperator' K Θ f x ≤
+    ENNReal.ofReal (C1_2 a q) * (volume G) ^ q'⁻¹ * (volume F) ^ q⁻¹ := by
+  sorry
 
 end

Carleson/CoverByBalls.lean

@@ -106,7 +106,9 @@ lemma BallsCoverBalls.pow_mul {a : ℝ} {k : ℕ} (h : ∀ r, BallsCoverBalls X
   case succ m h2 =>
     specialize h (r * a^m)
     rw[<- mul_assoc, mul_comm, <- mul_assoc] at h
-    rw[pow_succ, pow_succ, mul_comm (n^m) n]
+    norm_cast
+    ring_nf
+    rw[mul_comm a]
     rw[mul_comm] at h2
     norm_cast at h2
     exact BallsCoverBalls.trans h h2

Carleson/Defs.lean

@@ -153,6 +153,13 @@ def CarlesonOperator (K : X → X → ℂ) (Θ : Set C(X, ℂ)) (f : X → ℂ)
   ⨆ (Q ∈ Θ) (R₁ : ℝ) (R₂ : ℝ) (h1 : R₁ < R₂),
   ‖∫ y in {y | dist x y ∈ Ioo R₁ R₂}, K x y * f y * exp (I * Q y)‖
 
+/-- The (maximally truncated) polynomial Carleson operator `T`, ENNReal version -/
+--TODO: remove the last two suprema?
+--TODO: change definition of CarlesonOperater too
+def CarlesonOperator' (K : X → X → ℂ) (Θ : Set C(X, ℂ)) (f : X → ℂ) (x : X) : ENNReal :=
+  ⨆ (Q ∈ Θ) (R₁ : ℝ) (R₂ : ℝ) (_ : 0 < R₁) (_ : R₁ < R₂),
+  ↑‖∫ y in {y | dist x y ∈ Ioo R₁ R₂}, K x y * f y * exp (I * Q y)‖₊
+
 variable (X) in
 /-- A grid structure on `X`.
 I expect we prefer `𝓓 : ι → Set X` over `𝓓 : Set (Set X)`

Carleson/HomogeneousType.lean

@@ -3,6 +3,7 @@ import Carleson.ToMathlib.MeasureReal
 import Mathlib.MeasureTheory.Measure.Haar.Basic
 import Mathlib.MeasureTheory.Integral.Average
 import Mathlib.Analysis.SpecialFunctions.Log.Base
+import Mathlib.Analysis.NormedSpace.FiniteDimension
 
 open MeasureTheory Measure NNReal ENNReal Metric Filter Topology TopologicalSpace
 noncomputable section
@@ -63,8 +64,7 @@ lemma volume_ball_le_same (x : X) {r s r': ℝ} (hsp : s > 0) (hs : r' ≤ s * r
         _ = volume.real (ball x (2 * 2 ^ m * r)) := by ring_nf
         _ ≤ A * volume.real (ball x (2 ^ m * r)) := by rw[mul_assoc]; norm_cast; apply volume_ball_two_le_same
         _ ≤ A * (↑(A ^ m) * volume.real (ball x r)) := by gcongr
-        _ = A^(m+1) * volume.real (ball x r) := by
-          rw[← mul_assoc, pow_succ, mul_comm _ A]
+        _ = A^(Nat.succ m) * volume.real (ball x r) := by rw[<- mul_assoc, pow_succ']
 
   /-Show inclusion in larger ball-/
   have haux : s * r ≤ 2 ^ ⌈Real.log s / Real.log 2⌉₊ * r := by
@@ -143,13 +143,21 @@ lemma tendsto_average_zero {E} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X
 instance (n : ℕ) : Fact ((1 : ℝ) ≤ 2 ^ n) := ⟨by norm_cast; exact Nat.one_le_two_pow⟩
 
 /- ℝ^n is a space of homogenous type. -/
-instance {ι : Type*} [Fintype ι] : IsSpaceOfHomogeneousType (ι → ℝ) (2 ^ Fintype.card ι) := sorry
+--instance {ι : Type*} [Fintype ι] : IsSpaceOfHomogeneousType (ι → ℝ) (2 ^ Fintype.card ι) := sorry
 
 open FiniteDimensional
 /- Preferably we prove that in this form. -/
-instance {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] :
-    IsSpaceOfHomogeneousType E (2 ^ finrank ℝ E) := by
-  sorry
+instance {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasureSpace E] [BorelSpace E]:
+    IsSpaceOfHomogeneousType E (2 ^ finrank ℝ E) where
+      toMeasureSpace := inferInstance
+      toProperSpace := inferInstance
+      toBorelSpace := inferInstance
+      lt_top_of_isCompact := sorry
+      outerRegular := sorry
+      innerRegular := sorry
+      open_pos := sorry
+      volume_ball_two_le_same := sorry
+
 
 /- Maybe we can even generalize the field? (at least for `𝕜 = ℂ` as well) -/
 def NormedSpace.isSpaceOfHomogeneousType {𝕜 E : Type*} [NontriviallyNormedField 𝕜]