chore: further clean-ups and golfs (#121)

I won't have much Lean time in the next two weeks. Feel to split, polish and merge this PR, however you see fit.
fpvandoorn · Sep 10, 2024 · 8b76725 · 8b76725
2 parents f8193c5 + a0f58b0
commit 8b76725
Show file tree

Hide file tree

Showing 16 changed files with 208 additions and 406 deletions.
diff --git a/Carleson/Classical/Approximation.lean b/Carleson/Classical/Approximation.lean
@@ -8,7 +8,7 @@ import Mathlib.Analysis.PSeries
 
 noncomputable section
 
-open BigOperators Finset Real
+open Finset Real
 
 local notation "S_" => partialFourierSum
 

diff --git a/Carleson/Classical/Basic.lean b/Carleson/Classical/Basic.lean
@@ -7,7 +7,7 @@ import Mathlib.Analysis.Convolution
 
 import Carleson.Classical.Helper
 
-open BigOperators Finset Real
+open Finset Real
 
 noncomputable section
 

diff --git a/Carleson/Classical/ControlApproximationEffect.lean b/Carleson/Classical/ControlApproximationEffect.lean
@@ -610,8 +610,7 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
     _ ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (2 * π + 2) ^ (2 : ℝ)⁻¹) * (volume E') ^ (2 : ℝ)⁻¹ := by
       rcases h with hE' | hE'
       · exact rcarleson_exceptional_set_estimate_specific hδ h_measurable h_bound measurableSetE' (E'subset.trans Esubset) hE'
-      · refine rcarleson_exceptional_set_estimate_specific hδ ?_ conj_h_bound measurableSetE' (E'subset.trans Esubset) hE'
-        exact ContinuousStar.continuous_star.measurable.comp h_measurable
+      · exact rcarleson_exceptional_set_estimate_specific hδ (by fun_prop) conj_h_bound measurableSetE' (E'subset.trans Esubset) hE'
     _ ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (4 * π) ^ (2 : ℝ)⁻¹) * (volume E') ^ (2 : ℝ)⁻¹ := by
       gcongr
       · exact mul_nonneg hδ.le (C10_0_1_pos one_lt_two).le

diff --git a/Carleson/Classical/DirichletKernel.lean b/Carleson/Classical/DirichletKernel.lean
@@ -7,7 +7,7 @@ import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
 import Mathlib.Analysis.Convolution
 
 open scoped Real
-open BigOperators Finset Complex MeasureTheory
+open Finset Complex MeasureTheory
 
 noncomputable section
 

diff --git a/Carleson/Classical/VanDerCorput.lean b/Carleson/Classical/VanDerCorput.lean
@@ -94,11 +94,11 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
   push_neg at h
   have pi_div_n_pos : 0 < π / n := div_pos Real.pi_pos (Int.cast_pos.mpr n_pos)
   have integrand_continuous : Continuous (fun x ↦ cexp (I * ↑n * ↑x) * ϕ x)  :=
-    Continuous.mul (by continuity) h1.continuous
+    Continuous.mul (by fun_prop) h1.continuous
   have integrand_continuous2 : Continuous (fun x ↦ cexp (I * ↑n * (↑x + ↑π / ↑n)) * ϕ x) :=
-    Continuous.mul (by continuity) h1.continuous
+    Continuous.mul (by fun_prop) h1.continuous
   have integrand_continuous3 : Continuous (fun (x : ℝ) ↦ cexp (I * n * x) * ϕ (x - π / n)) :=
-    Continuous.mul (by continuity) (h1.continuous.comp (by continuity))
+    Continuous.mul (by fun_prop) (h1.continuous.comp (by continuity))
   calc _
     _ = ‖∫ (x : ℝ) in a..b, (1 / 2 * (I * n * x).exp - 1 / 2 * (I * ↑n * (↑x + ↑π / ↑n)).exp) * ϕ x‖ := by
       congr

diff --git a/Carleson/Discrete/Defs.lean b/Carleson/Discrete/Defs.lean
@@ -1,7 +1,7 @@
 import Carleson.Forest
 import Carleson.MinLayerTiles
 
-open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology
+open MeasureTheory Measure NNReal Metric Set
 open scoped ENNReal
 open Classical -- We use quite some `Finset.filter`
 noncomputable section

diff --git a/Carleson/Discrete/ExceptionalSet.lean b/Carleson/Discrete/ExceptionalSet.lean
@@ -1,7 +1,7 @@
 import Carleson.Discrete.Defs
 import Carleson.HardyLittlewood
 
-open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology
+open MeasureTheory Measure NNReal Metric Set
 open scoped ENNReal
 open Classical -- We use quite some `Finset.filter`
 noncomputable section

diff --git a/Carleson/Discrete/Forests.lean b/Carleson/Discrete/Forests.lean
@@ -1,6 +1,6 @@
 import Carleson.Discrete.ExceptionalSet
 
-open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology
+open MeasureTheory Measure NNReal Metric Complex Set
 open scoped ENNReal
 open Classical -- We use quite some `Finset.filter`
 noncomputable section

diff --git a/Carleson/FinitaryCarleson.lean b/Carleson/FinitaryCarleson.lean
@@ -1,7 +1,7 @@
 import Carleson.Discrete.Forests
 import Carleson.TileExistence
 
-open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology Classical
+open MeasureTheory Measure NNReal Metric Complex Set Classical
 open scoped ENNReal
 noncomputable section
 

diff --git a/Carleson/LinearizedMetricCarleson.lean b/Carleson/LinearizedMetricCarleson.lean
@@ -1,7 +1,7 @@
 import Carleson.Defs
 
-open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators
-open scoped ENNReal
+open MeasureTheory Set
+
 noncomputable section
 
 /-- The constant used in `linearized_metric_carleson`.

diff --git a/Carleson/MetricCarleson.lean b/Carleson/MetricCarleson.lean
@@ -1,7 +1,7 @@
 import Carleson.Defs
 
-open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators
-open scoped ENNReal
+open MeasureTheory Set
+
 noncomputable section
 
 /-- The constant used in `metric_carleson`.

diff --git a/Carleson/Psi.lean b/Carleson/Psi.lean
@@ -80,12 +80,10 @@ lemma ψ_formula₄ {x : ℝ} (hx : x ≥ 1 / 2) : ψ D x = 0 :=
   max_eq_left <| (min_le_right _ _).trans <| (min_le_right _ _).trans (by linarith)
 ---------------------------------------------
 
-lemma psi_zero : ψ D 0 = 0 :=
-  ψ_formula₀ (div_nonneg one_pos.le <| mul_nonneg four_pos.le (Nat.cast_nonneg D))
+lemma psi_zero : ψ D 0 = 0 := ψ_formula₀ (by positivity)
 
-lemma continuous_ψ : Continuous (ψ D) :=
-  continuous_const.max <| continuous_const.min <| ((continuous_mul_left _).sub continuous_const).min
-    (continuous_const.sub (continuous_mul_left 4))
+lemma continuous_ψ : Continuous (ψ D) := by
+  unfold ψ; fun_prop
 
 include hD in
 lemma support_ψ : support (ψ D) = Ioo (4 * D : ℝ)⁻¹ 2⁻¹ := by
@@ -657,8 +655,7 @@ lemma integrable_Ks_x {s : ℤ} {x : X} (hD : 1 < (D : ℝ)) : Integrable (Ks s
   rw [this]
   refine Integrable.bdd_mul ?_ (Measurable.aestronglyMeasurable ?_) ?_
   · apply Continuous.integrable_of_hasCompactSupport
-    · exact continuous_ofReal.comp <| continuous_ψ.comp <| continuous_const.mul <|
-        continuous_const.dist continuous_id
+    · exact continuous_ofReal.comp <| continuous_ψ.comp <| (by fun_prop)
     · apply HasCompactSupport.of_support_subset_isCompact (isCompact_closedBall x (D ^ s / 2))
       intro y hy
       rw [mem_support, ne_eq, ofReal_eq_zero, ← ne_eq, ← mem_support, support_ψ (D1 X)] at hy