Merge branch 'master' of https://github.com/ldiedering/carleson

Carleson.lean

@@ -1,3 +1,4 @@
+import Carleson.Carleson
 import Carleson.CoverByBalls
 import Carleson.Defs
 import Carleson.HomogeneousType
@@ -6,10 +7,12 @@ import Carleson.Proposition2
 import Carleson.Proposition3
 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.ToMathlib.Finiteness
 import Carleson.ToMathlib.Finiteness.Attr
 import Carleson.ToMathlib.MeasureReal

Carleson/Carleson.lean

@@ -68,10 +68,10 @@ theorem Int.le_ceil_iff (c : ℝ) (z : ℤ) : z ≤ ⌈c⌉ ↔ z - 1 < c := by
 lemma mem_nonzeroS_iff {i : ℤ} {x : ℝ} (hx : 0 < x) (hD : 1 < D) :
     i ∈ nonzeroS D x ↔ (D ^ i * x) ∈ Ioo (4 * D)⁻¹ 2⁻¹ := by
   rw [Set.mem_Ioo, nonzeroS, Finset.mem_Icc]
-  simp [Int.floor_le_iff, Int.le_ceil_iff]
-  rw [← lt_div_iff hx, mul_comm D⁻¹, ← div_lt_div_iff hx (by positivity)]
-  rw [← Real.logb_inv, ← Real.logb_inv]
-  rw [div_inv_eq_mul, ← zpow_add_one₀ (by positivity)]
+  simp only [Int.floor_le_iff, neg_add_rev, Int.le_ceil_iff, lt_add_neg_iff_add_lt, sub_add_cancel,
+    mul_inv_rev]
+  rw [← lt_div_iff hx, mul_comm D⁻¹, ← div_lt_div_iff hx (by positivity), ← Real.logb_inv,
+    ← Real.logb_inv, div_inv_eq_mul, ← zpow_add_one₀ (by positivity)]
   simp_rw [← Real.rpow_intCast]
   rw [Real.lt_logb_iff_rpow_lt hD (by positivity), Real.logb_lt_iff_lt_rpow hD (by positivity)]
   simp [div_eq_mul_inv, mul_comm]

Carleson/CoverByBalls.lean

@@ -65,7 +65,7 @@ lemma CoveredByBalls.zero_right : CoveredByBalls s n 0 ↔ s = ∅ := by
     intro hs
     have h21 : (∅ : Finset X).card ≤ n := by exact tsub_add_cancel_iff_le.mp rfl
     have h22 : s ⊆ ⋃ x ∈ (∅ : Finset X), ball x 0 := by
-      simp
+      simp only [not_mem_empty, ball_zero, Set.iUnion_of_empty, Set.iUnion_empty]
       exact Set.subset_empty_iff.mpr hs
     exact ⟨(∅ : Finset X), h21, h22⟩
   exact { mp := h1, mpr := h2 }

Carleson/Theorem1_1/Approximation.lean

@@ -5,7 +5,6 @@ import Carleson.HomogeneousType
 import Carleson.Theorem1_1.Basic
 
 import Mathlib.Analysis.Fourier.AddCircle
-import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Analysis.Convolution
 import Mathlib.Analysis.Calculus.BumpFunction.Convolution
 import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
@@ -59,7 +58,7 @@ lemma closeSmoothApprox {f : ℝ → ℂ} (unicontf : UniformContinuous f) {ε :
     apply ContDiffBump.dist_normed_convolution_le
     . exact unicontf.continuous.aestronglyMeasurable
     . intro y hy
-      simp at hy
+      simp only [Metric.mem_ball] at hy
       exact (hδ hy).le
 
 /- Slightly different version-/
@@ -90,7 +89,7 @@ lemma closeSmoothApproxPeriodic {f : ℝ → ℂ} (unicontf : UniformContinuous
     apply ContDiffBump.dist_normed_convolution_le
     . exact unicontf.continuous.aestronglyMeasurable
     . intro y hy
-      simp at hy
+      simp only [Metric.mem_ball] at hy
       exact (hδ hy).le
 
 /- Inspired by mathlib : NNReal.summable_of_le-/
@@ -120,7 +119,7 @@ lemma summable_of_le_on_nonzero {f g : ℤ → ℝ} (hgpos : 0 ≤ g) (hgf : ∀
     rw [f'def]
     by_cases h : i = 0
     . simp [h]
-    . simp [h]
+    . simp only [h, ↓reduceIte]
       exact hgf i h
   apply Real.summable_of_le hgpos this
 
@@ -133,7 +132,6 @@ lemma summable_of_le_on_nonzero {f g : ℤ → ℝ} (hgpos : 0 ≤ g) (hgf : ∀
   rw [f'def]
   simp [hb]
 
-
   lemma continuous_bounded {f : ℝ → ℂ} (hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))) : ∃ C, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C := by
     have interval_compact := (@isCompact_Icc ℝ _ _ _ 0 (2 * Real.pi))
     have abs_f_continuousOn := Complex.continuous_abs.comp_continuousOn hf
@@ -173,7 +171,7 @@ lemma fourierCoeffOn_bound {f : ℝ → ℂ} (f_continuous : Continuous f) : ∃
     _ = ∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), ‖f x‖ := by
       congr
       ext x
-      simp
+      simp only [norm_mul, Complex.norm_eq_abs]
       rw [mul_assoc, mul_comm Complex.I]
       norm_cast
       rw [Complex.abs_exp_ofReal_mul_I]
@@ -284,7 +282,8 @@ lemma int_sum_nat {β : Type} [AddCommGroup β] [TopologicalSpace β] [Continuou
     rw [this, sum_insert, sum_insert, ih, ←add_assoc]
     symm
     rw [sum_range_succ, add_comm, ←add_assoc, add_comm]
-    simp
+    simp only [Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg, Nat.succ_eq_add_one,
+      Int.ofNat_eq_coe, add_right_inj]
     rw [add_comm]
     . simp
     . norm_num
@@ -312,13 +311,13 @@ lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : Function.
     have summable_maj : Summable maj := by
       by_cases Ceq0 : C = 0
       . rw [maj_def, Ceq0]
-        simp
+        simp only [one_div, mul_zero]
         exact summable_zero
       . rw [← summable_div_const_iff Ceq0]
         convert Real.summable_one_div_int_pow.mpr one_lt_two using 1
         rw [maj_def]
         ext i
-        simp
+        simp only [one_div]
         rw [mul_div_cancel_right₀]
         exact Ceq0
     rw [summable_congr @fourierCoeff_correspondence, ←summable_norm_iff]
@@ -344,7 +343,7 @@ lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : Function.
   convert this.le using 2
   congr 1
   . rw [g_def]
-    simp
+    simp only [ContinuousMap.coe_mk]
     rw [AddCircle.liftIco_coe_apply]
     rw [zero_add]
     exact hx

Carleson/Theorem1_1/Basic.lean

@@ -20,32 +20,31 @@ def partialFourierSum (f : ℝ → ℂ) (N : ℕ) : ℝ → ℂ := fun x ↦ ∑
 @[simp]
 lemma fourierCoeffOn_mul {a b : ℝ} {hab : a < b} {f: ℝ → ℂ} {c : ℂ} {n : ℤ} : fourierCoeffOn hab (fun x ↦ c * f x) n =
     c * (fourierCoeffOn hab f n):= by
-  rw [fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral]
-  simp
-  rw [←mul_assoc, mul_comm c, mul_assoc _ c, mul_comm c, ←intervalIntegral.integral_mul_const]
+  simp only [fourierCoeffOn_eq_integral, one_div, fourier_apply, neg_smul, fourier_neg',
+    fourier_coe_apply', Complex.ofReal_sub, smul_eq_mul, Complex.real_smul, Complex.ofReal_inv]
+  rw [← mul_assoc, mul_comm c, mul_assoc _ c, mul_comm c, ← intervalIntegral.integral_mul_const]
   congr
   ext x
   ring
 
 @[simp]
 lemma fourierCoeffOn_neg {a b : ℝ} {hab : a < b} {f: ℝ → ℂ} {n : ℤ} : fourierCoeffOn hab (-f) n =
-    - (fourierCoeffOn hab f n):= by
-  rw [fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral]
-  simp
+    - (fourierCoeffOn hab f n):= by simp [fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral]
 
 @[simp]
 lemma fourierCoeffOn_add {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hg : IntervalIntegrable g MeasureTheory.volume a b) :
     fourierCoeffOn hab (f + g) n = fourierCoeffOn hab f n + fourierCoeffOn hab g n:= by
-  rw [fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral]
-  simp
-  rw [←mul_add, ←intervalIntegral.integral_add]
+  simp only [fourierCoeffOn_eq_integral, one_div, fourier_apply, neg_smul, fourier_neg',
+    fourier_coe_apply', Complex.ofReal_sub, Pi.add_apply, smul_eq_mul, Complex.real_smul,
+    Complex.ofReal_inv]
+  rw [← mul_add, ← intervalIntegral.integral_add]
   congr
   ext x
   ring
-  . apply IntervalIntegrable.continuousOn_mul hf
+  . apply hf.continuousOn_mul
     apply Continuous.continuousOn
     continuity
-  . apply IntervalIntegrable.continuousOn_mul hg
+  . apply hg.continuousOn_mul
     apply Continuous.continuousOn
     continuity
 
@@ -58,16 +57,15 @@ lemma fourierCoeffOn_sub {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ}
 @[simp]
 lemma partialFourierSum_add {f g : ℝ → ℂ} {N : ℕ} (hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)): partialFourierSum (f + g) N = partialFourierSum f N + partialFourierSum g N := by
   ext x
-  simp
-  rw [partialFourierSum, partialFourierSum, partialFourierSum, ←sum_add_distrib]
+  simp [partialFourierSum, partialFourierSum, partialFourierSum, ← sum_add_distrib]
   congr
   ext n
   rw [fourierCoeffOn_add hf hg, add_mul]
 
 @[simp]
 lemma partialFourierSum_sub {f g : ℝ → ℂ} {N : ℕ} (hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)): partialFourierSum (f - g) N = partialFourierSum f N - partialFourierSum g N := by
   ext x
-  simp
+  simp only [Pi.sub_apply]
   rw [partialFourierSum, partialFourierSum, partialFourierSum, ←sum_sub_distrib]
   congr
   ext n
@@ -82,9 +80,7 @@ lemma partialFourierSum_mul {f: ℝ → ℂ} {a : ℂ} {N : ℕ}: partialFourier
   ext n
   rw [fourierCoeffOn_mul, mul_assoc]
 
-lemma fourier_periodic {n : ℤ} : Function.Periodic (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * Real.pi))) (2 * Real.pi) := by
-  intro x
-  simp
+lemma fourier_periodic {n : ℤ} : Function.Periodic (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * Real.pi))) (2 * Real.pi) := by simp
 
 lemma partialFourierSum_periodic {f : ℝ → ℂ} {N : ℕ} : Function.Periodic (partialFourierSum f N) (2 * Real.pi) := by
   rw [Function.Periodic]
@@ -97,8 +93,7 @@ lemma partialFourierSum_periodic {f : ℝ → ℂ} {N : ℕ} : Function.Periodic
 
 /-TODO: Add lemma Periodic.uniformContinuous_of_continuous. -/
 lemma fourier_uniformContinuous {n : ℤ} : UniformContinuous (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * Real.pi))) := by
-  rw [fourier]
-  simp
+  simp [fourier]
   --apply Complex.exp_mul_I_periodic.
   sorry
 

Carleson/Theorem1_1/Carleson_on_the_real_line.lean

@@ -6,14 +6,11 @@ import Carleson.Theorem1_1.Basic
 import Carleson.Theorem1_1.Hilbert_kernel
 import Carleson.Theorem1_1.CarlesonOperatorReal
 
-
 --import Mathlib.Tactic
 import Mathlib.Analysis.Fourier.AddCircle
-import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.Analysis.SpecialFunctions.Integrals
 
-
 noncomputable section
 
 --#lint
@@ -54,8 +51,7 @@ lemma h1 : 2 ∈ Set.Ioc 1 (2 : ℝ) := by simp
 lemma h2 : Real.IsConjExponent 2 2 := by rw [Real.isConjExponent_iff_eq_conjExponent] <;> norm_num
 
 lemma localOscillation_on_emptyset {X : Type} [PseudoMetricSpace X] {f g : C(X, ℂ)} : localOscillation ∅ f g = 0 := by
-  rw [localOscillation]
-  simp
+  simp [localOscillation]
 
 lemma localOscillation_on_empty_ball {X : Type} [PseudoMetricSpace X] {x : X} {f g : C(X, ℂ)} {R : ℝ} (R_nonpos : R ≤ 0):
     localOscillation (Metric.ball x R) f g = 0 := by
@@ -227,10 +223,9 @@ lemma bciSup_of_emptyset  {α : Type} [ConditionallyCompleteLattice α] {ι : Ty
     ⨆ i ∈ (∅ : Set ι), f i = sSup ∅ := by
   rw [iSup]
   convert csSup_singleton _
-  have : ∀ i : ι, IsEmpty (i ∈ ∅) := by
+  have : ∀ i : ι, IsEmpty (i ∈ (∅ : Set ι)) := by
     intro i
     simp
-    apply Set.not_mem_empty
   have : (fun (i : ι) ↦ ⨆ (_ : i ∈ (∅ : Set ι)), f i) = fun i ↦ sSup ∅ := by
     ext i
     --rw [csSup_empty]

Carleson/Theorem1_1/ClassicalCarleson.lean

@@ -33,8 +33,7 @@ theorem classical_carleson {f : ℝ → ℂ}
   have h_periodic : Function.Periodic h (2 * Real.pi) := Function.Periodic.sub periodic_f₀ periodicf
   have h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε' := by
     intro x _
-    rw [hdef]
-    simp
+    simp [hdef]
     rw [←Complex.dist_eq, dist_comm, Complex.dist_eq]
     exact hf₀ x
 

Carleson/Theorem1_1/Dirichlet_kernel.lean

@@ -11,7 +11,6 @@ open Complex
 
 noncomputable section
 
-
 def dirichletKernel (N : ℕ) : ℝ → ℂ := fun x ↦ ∑ n in Icc (-Int.ofNat ↑N) N, fourier n (x : AddCircle (2 * Real.pi))
 
 def dirichletKernel' (N : ℕ) : ℝ → ℂ := fun x ↦ (exp (I * N * x) / (1 - exp (-I * x)) + exp (-I * N * x) / (1 - exp (I * x)))
@@ -34,37 +33,34 @@ lemma dirichletKernel_eq {N : ℕ} {x : ℝ} (h : cexp (I * x) ≠ 1) : dirichle
       = cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by
     calc (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x
       _ = ∑ n in Icc (-Int.ofNat N) ↑N, (cexp ((n + 1 / 2) * I * ↑x) - cexp ((n - 1 / 2) * I * ↑x)) := by
-        rw [dirichletKernel]
-        rw [mul_sum]
+        rw [dirichletKernel, mul_sum]
         congr
         ext n
-        simp
-        rw [sub_mul, ←exp_add, ←exp_add]
+        simp [sub_mul, ← exp_add, ← exp_add]
         congr <;>
         . ring_nf
           congr 1
           rw [mul_assoc, mul_assoc]
           congr
-          rw [←mul_assoc, mul_comm, ←mul_assoc, inv_mul_cancel, one_mul]
+          rw [← mul_assoc, mul_comm, ← mul_assoc, inv_mul_cancel, one_mul]
           norm_cast
           exact Real.pi_pos.ne.symm
       _ = ∑ n in Icc (-Int.ofNat N) ↑N, cexp ((n + 1 / 2) * I * ↑x) - ∑ n in Icc (-Int.ofNat N) ↑N, cexp ((n - 1 / 2) * I * ↑x) := by
         rw [sum_sub_distrib]
       _ = cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by
-        rw [←sum_Ico_add_eq_sum_Icc, ←sum_Ioc_add_eq_sum_Icc, add_sub_add_comm]
+        rw [← sum_Ico_add_eq_sum_Icc, ← sum_Ioc_add_eq_sum_Icc, add_sub_add_comm]
         symm
-        rw [←zero_add (cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x))]
+        rw [← zero_add (cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x))]
         congr
         symm
         rw [sub_eq_zero]
-        conv => lhs; rw [←Int.add_sub_cancel (-Int.ofNat N) 1, sub_eq_add_neg, ←Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ←sum_Ico_add']
+        conv => lhs; rw [← Int.add_sub_cancel (-Int.ofNat N) 1, sub_eq_add_neg, ← Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ← sum_Ico_add']
         congr
         . ext n
-          rw [mem_Ico, mem_Ioc, Int.lt_iff_add_one_le, add_le_add_iff_right, ←mem_Icc, Int.lt_iff_add_one_le, ←mem_Icc]
+          rw [mem_Ico, mem_Ioc, Int.lt_iff_add_one_le, add_le_add_iff_right, ← mem_Icc, Int.lt_iff_add_one_le, ← mem_Icc]
         . ext n
           congr
-          simp
-          rw [add_assoc, sub_eq_add_neg]
+          simp [add_assoc, sub_eq_add_neg]
           congr
           norm_num
         . rw [neg_add_rev, add_comm, Int.ofNat_eq_coe, Int.cast_neg, sub_eq_add_neg]
@@ -75,14 +71,14 @@ lemma dirichletKernel_eq {N : ℕ} {x : ℝ} (h : cexp (I * x) ≠ 1) : dirichle
     rw [sub_eq_zero] at h
     calc cexp (I * ↑x)
       _ = cexp (1 / 2 * I * ↑x) * cexp (1 / 2 * I * ↑x) := by
-        rw [←exp_add]
+        rw [← exp_add]
         congr
-        rw [mul_assoc, ←mul_add]
+        rw [mul_assoc, ← mul_add]
         ring
       _ = cexp (1 / 2 * I * ↑x) * cexp (-1 / 2 * I * ↑x) := by
         congr
       _ = 1 := by
-        rw [←exp_add]
+        rw [← exp_add]
         ring_nf
         exact exp_zero
   rw [dirichletKernel']
@@ -94,14 +90,14 @@ lemma dirichletKernel_eq {N : ℕ} {x : ℝ} (h : cexp (I * x) ≠ 1) : dirichle
     . contrapose! h
       rwa [sub_eq_zero, neg_mul, exp_neg, eq_comm, inv_eq_one] at h
     ring_nf
-    rw [←exp_add, ←exp_add, ←exp_add]
+    rw [← exp_add, ← exp_add, ← exp_add]
     congr 2 <;> ring
   . rw [mul_div]
     apply eq_div_of_mul_eq
     . contrapose! h
       rwa [sub_eq_zero, eq_comm] at h
     ring_nf
-    rw [←exp_add, ←exp_add, ←exp_add, neg_add_eq_sub]
+    rw [← exp_add, ← exp_add, ← exp_add, neg_add_eq_sub]
     congr 2 <;> ring
 
 lemma dirichletKernel'_eq_zero {N : ℕ} {x : ℝ} (h : cexp (I * x) = 1) : dirichletKernel' N x = 0 := by
@@ -163,15 +159,15 @@ lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x :
       ext n
       rw [fourierCoeffOn_eq_integral, smul_mul_assoc]
     _ = (1 / (2 * Real.pi)) * ∑ n in Icc (-Int.ofNat N) ↑N, ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by
-      rw [←smul_sum, real_smul, sub_zero]
+      rw [← smul_sum, real_smul, sub_zero]
       norm_cast
     _ = (1 / (2 * Real.pi)) * ∑ n in Icc (-Int.ofNat N) ↑N, ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y) * (fourier n) ↑x)) := by
       congr
       ext n
       symm
       apply intervalIntegral.integral_mul_const
     _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), ∑ n in Icc (-Int.ofNat N) ↑N, (fourier (-n)) y • f y * (fourier n) x := by
-      rw [←intervalIntegral.integral_finset_sum]
+      rw [← intervalIntegral.integral_finset_sum]
       intro n _
       apply IntervalIntegrable.mul_const
       apply IntervalIntegrable.continuousOn_mul h fourier_uniformContinuous.continuous.continuousOn
@@ -194,7 +190,6 @@ lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x :
       field_simp
       rw [mul_sub, sub_eq_neg_add]
 
-
 lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) :
     partialFourierSum f N x = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel' N (x - y)  := by
   have : (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel' N (x - y) = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel N (x - y) := by