Golf #36 (#84)

Golf #36

Carleson/Defs.lean

@@ -163,22 +163,10 @@ def iLipNorm {𝕜} [NormedField 𝕜] (ϕ : X → 𝕜) (x₀ : X) (R : ℝ) :
   (⨆ x ∈ ball x₀ R, ‖ϕ x‖) + R * ⨆ (x : X) (y : X) (h : x ≠ y), ‖ϕ x - ϕ y‖ / dist x y
 
 lemma iLipNorm_nonneg {𝕜} [NormedField 𝕜] {ϕ : X → 𝕜} {x₀ : X} {R : ℝ} (hR : 0 ≤ R) :
-    0 ≤ iLipNorm ϕ x₀ R := by
-  unfold iLipNorm
-  apply add_nonneg
-  . apply Real.iSup_nonneg
-    intro x
-    apply Real.iSup_nonneg
-    intro _
-    apply norm_nonneg
-  . apply mul_nonneg hR
-    apply Real.iSup_nonneg
-    intro x
-    apply Real.iSup_nonneg
-    intro y
-    apply Real.iSup_nonneg
-    intro _
-    apply div_nonneg (norm_nonneg _) dist_nonneg
+    0 ≤ iLipNorm ϕ x₀ R :=
+  add_nonneg (Real.iSup_nonneg fun _ ↦ Real.iSup_nonneg fun _ ↦ norm_nonneg _)
+    (mul_nonneg hR (Real.iSup_nonneg fun _ ↦ Real.iSup_nonneg fun _ ↦ Real.iSup_nonneg
+    fun _ ↦ div_nonneg (norm_nonneg _) dist_nonneg))
 
 variable (X) in
 /-- Θ is τ-cancellative. `τ` will usually be `1 / a` -/

Carleson/Theorem1_1/Basic.lean

@@ -99,15 +99,14 @@ lemma Function.Periodic.uniformContinuous_of_continuous {f : ℝ → ℂ} {T : 
   constructor <;> linarith [ha.1, ha.2]
 
 
-lemma fourier_uniformContinuous {n : ℤ} : UniformContinuous (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * Real.pi))) := by
-  apply fourier_periodic.uniformContinuous_of_continuous Real.two_pi_pos
-  apply Continuous.continuousOn
+lemma fourier_uniformContinuous {n : ℤ} :
+    UniformContinuous (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * Real.pi))) := by
+  apply fourier_periodic.uniformContinuous_of_continuous Real.two_pi_pos (Continuous.continuousOn _)
   continuity
 
 lemma partialFourierSum_uniformContinuous {f : ℝ → ℂ} {N : ℕ} : UniformContinuous (partialFourierSum f N) := by
   apply partialFourierSum_periodic.uniformContinuous_of_continuous Real.two_pi_pos
-  apply Continuous.continuousOn
-  apply continuous_finset_sum
+    (Continuous.continuousOn (continuous_finset_sum _ _))
   continuity
 
 theorem strictConvexOn_cos_Icc : StrictConvexOn ℝ (Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2)) Real.cos := by

Carleson/Theorem1_1/CarlesonOperatorReal.lean

@@ -14,64 +14,47 @@ lemma annulus_real_eq {x r R: ℝ} (r_nonneg : 0 ≤ r) : {y | dist x y ∈ Set.
     Set.mem_setOf_eq, Set.mem_union]
   constructor
   · rintro ⟨(h₀ | h₀), h₁, h₂⟩
-    · left
-      constructor <;> linarith
-    · right
-      constructor <;> linarith
+    · left; constructor <;> linarith
+    · right; constructor <;> linarith
   · rintro (⟨h₀, h₁⟩ | ⟨h₀, h₁⟩)
-    · constructor
-      · left
-        linarith
-      · constructor <;> linarith
-    · constructor
-      · right
-        linarith
-      · constructor <;> linarith
+    · exact ⟨by left; linarith, by constructor <;> linarith⟩
+    · exact ⟨by right; linarith, by constructor <;> linarith⟩
 
-lemma annulus_real_volume {x r R : ℝ} (hr : r ∈ Set.Icc 0 R) : MeasureTheory.volume {y | dist x y ∈ Set.Ioo r R} = ENNReal.ofReal (2 * (R - r)) := by
+lemma annulus_real_volume {x r R : ℝ} (hr : r ∈ Set.Icc 0 R) :
+    MeasureTheory.volume {y | dist x y ∈ Set.Ioo r R} = ENNReal.ofReal (2 * (R - r)) := by
   rw [annulus_real_eq hr.1, MeasureTheory.measure_union _ measurableSet_Ioo, Real.volume_Ioo, Real.volume_Ioo, ← ENNReal.ofReal_add (by linarith [hr.2]) (by linarith [hr.2])]
   ring_nf
   rw [Set.disjoint_iff]
   intro y hy
   linarith [hy.1.2, hy.2.1, hr.1]
 
-
-lemma annulus_measurableSet {x r R : ℝ} : MeasurableSet {y | dist x y ∈ Set.Ioo r R} := measurableSet_preimage (measurable_const.dist measurable_id) measurableSet_Ioo
+lemma annulus_measurableSet {x r R : ℝ} : MeasurableSet {y | dist x y ∈ Set.Ioo r R} :=
+  measurableSet_preimage (measurable_const.dist measurable_id) measurableSet_Ioo
 
 lemma sup_eq_sup_dense_of_continuous {f : ℝ → ENNReal} {S : Set ℝ} (D : Set ℝ) (hS : IsOpen S) (hD: Dense D) (hf : ContinuousOn f S) :
     ⨆ r ∈ S, f r = ⨆ r ∈ (S ∩ D), f r := by
   --Show two inequalities, one is trivial
-  apply le_antisymm _ (biSup_mono Set.inter_subset_left)
-  apply le_of_forall_ge_of_dense
-  intro c hc
+  refine le_antisymm (le_of_forall_ge_of_dense fun c hc ↦ ?_) (biSup_mono Set.inter_subset_left)
   rw [lt_iSup_iff] at hc
   rcases hc with ⟨x, hx⟩
   rw [lt_iSup_iff] at hx
   rcases hx with ⟨xS, hx⟩
   have : IsOpen (S ∩ f ⁻¹' (Set.Ioi c)) := hf.isOpen_inter_preimage hS isOpen_Ioi
   have : Set.Nonempty ((S ∩ f ⁻¹' (Set.Ioi c)) ∩ D) := by
-    apply hD.inter_open_nonempty
-    exact this
+    apply hD.inter_open_nonempty _ this _
     use x, xS
     simpa
   rcases this with ⟨y, hy⟩
   rw [Set.mem_inter_iff, Set.mem_inter_iff, Set.mem_preimage, Set.mem_Ioi] at hy
-  apply hy.1.2.le.trans
-  apply le_biSup
-  exact ⟨hy.1.1, hy.2⟩
+  exact hy.1.2.le.trans (le_biSup _ ⟨hy.1.1, hy.2⟩)
 
-lemma helper {n : ℤ} {f : ℝ → ℂ} (hf : Measurable f) : Measurable (Function.uncurry fun x y ↦ f y * K x y * (Complex.I * n * y).exp) := by
-  apply Measurable.mul
-  apply Measurable.mul
-  apply hf.comp measurable_snd
-  exact Hilbert_kernel_measurable
-  apply Measurable.cexp
-  apply Measurable.mul measurable_const
-  apply Complex.measurable_ofReal.comp measurable_snd
+lemma helper {n : ℤ} {f : ℝ → ℂ} (hf : Measurable f) :
+    Measurable (Function.uncurry fun x y ↦ f y * K x y * (Complex.I * n * y).exp) :=
+  Measurable.mul (Measurable.mul (hf.comp measurable_snd) Hilbert_kernel_measurable)
+  (measurable_const.mul (Complex.measurable_ofReal.comp measurable_snd)).cexp
 
 local notation "T" => CarlesonOperatorReal K
 
-
 lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurable f) {B : ℝ} (f_bounded : ∀ x, ‖f x‖ ≤ B) : Measurable (T f):= by
   --TODO: clean up proof
   apply measurable_iSup
@@ -97,17 +80,13 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
     . rw [Rat.denseEmbedding_coe_real.dense_image]
       exact dense_univ
     . rw [Set.countable_coe_iff, Qdef, Set.image_univ]
-      apply Set.countable_range
+      exact Set.countable_range _
   have : (fun x ↦ ⨆ (r ∈ Set.Ioo 0 1), G x r) = (fun x ↦ ⨆ (r ∈ (Set.Ioo 0 1) ∩ Q), G x r) := by
     ext x
     rw [sup_eq_sup_dense_of_continuous Q isOpen_Ioo hQ.1]
-    intro r hr
-    apply ContinuousAt.continuousWithinAt
-    apply ContinuousAt.comp
-    . apply Continuous.continuousAt
-      apply EReal.continuous_coe_ennreal_iff.mp
-      apply EReal.continuous_coe_iff.mpr (continuous_iff_le_induced.mpr fun U a ↦ a)
-    apply ContinuousAt.nnnorm
+    refine fun r hr ↦ ContinuousAt.continuousWithinAt (ContinuousAt.comp (Continuous.continuousAt
+      (EReal.continuous_coe_ennreal_iff.mp (EReal.continuous_coe_iff.mpr
+      (continuous_iff_le_induced.mpr fun U a ↦ a)))) (ContinuousAt.nnnorm ?_))
     set S := Set.Ioo (r / 2) (2 * r) with Sdef
     set bound := fun y ↦ ‖F x (r / 2) y‖ with bound_def
     have h_bound : ∀ᶠ (s : ℝ) in nhds r, ∀ᵐ (a : ℝ), ‖F x s a‖ ≤ bound a := by
@@ -155,8 +134,7 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
       . rw [annulus_real_volume (by constructor <;> linarith [hr.1, hr.2])]
         exact ENNReal.ofReal_ne_top
       . --measurability
-        apply Measurable.aestronglyMeasurable
-        apply Measurable.norm (Measurable.of_uncurry_left (helper f_measurable))
+        apply ((Measurable.of_uncurry_left (helper f_measurable)).norm).aestronglyMeasurable
       . --interesting part
         rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
         simp_rw [norm_norm]
@@ -179,9 +157,8 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
         . push_neg at h
           rw [Set.indicator_apply, ite_cond_eq_false, Set.indicator_apply, ite_cond_eq_false]
           all_goals
-            simp
-            intro _
-            exact h
+            simp only [Set.mem_setOf_eq, eq_iff_iff, iff_false, not_and, not_lt]
+            exact fun _ ↦ h
       have contOn2 : ∀ (y : ℝ), ContinuousOn (fun s ↦ F x s y) (Set.Ioi (min (dist x y) 1)) := by
         intro y
         rw [continuousOn_iff_continuous_restrict]
@@ -208,10 +185,10 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
       have contOn : ∀ y, ∀ t ≠ dist x y, ContinuousAt (fun s ↦ F x s y) t := by
         intro y t ht
         by_cases h : t < dist x y
-        . apply (contOn1 y).continuousAt (Iio_mem_nhds h)
+        . exact_mod_cast (contOn1 y).continuousAt (Iio_mem_nhds h)
         . push_neg at h
-          apply ContinuousOn.continuousAt (contOn2 y)
-          exact Ioi_mem_nhds ((min_le_left _ _).trans_lt (lt_of_le_of_ne h ht.symm))
+          exact ContinuousOn.continuousAt (contOn2 y) (Ioi_mem_nhds
+            ((min_le_left _ _).trans_lt (lt_of_le_of_ne h ht.symm)))
       have subset_finite : {y | ¬ContinuousAt (fun s ↦ F x s y) r} ⊆ ({x - r, x + r} : Finset ℝ) := by
         intro y hy
         have : dist x y = r := by
@@ -224,24 +201,18 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
         . left; linarith
         . right; linarith
       rw [MeasureTheory.ae_iff]
-      apply MeasureTheory.measure_mono_null subset_finite
-      apply Finset.measure_zero
-    . apply Filter.eventually_of_forall
-      intro r
-      apply ((Measurable.of_uncurry_left (helper f_measurable)).indicator annulus_measurableSet).aestronglyMeasurable
+      exact MeasureTheory.measure_mono_null subset_finite (Finset.measure_zero _ _)
+    . exact Filter.eventually_of_forall fun r ↦ ((Measurable.of_uncurry_left
+        (helper f_measurable)).indicator annulus_measurableSet).aestronglyMeasurable
   rw [this]
-  apply measurable_biSup
+  apply measurable_biSup _
   apply Set.Countable.mono Set.inter_subset_right hQ.2
   intro r _
-  --measurability
-  apply measurable_coe_nnreal_ennreal.comp
-  apply measurable_nnnorm.comp
+  apply measurable_coe_nnreal_ennreal.comp (measurable_nnnorm.comp _)
   rw [← stronglyMeasurable_iff_measurable]
   apply MeasureTheory.StronglyMeasurable.integral_prod_right
   rw [stronglyMeasurable_iff_measurable, Fdef]
-  apply Measurable.indicator (helper f_measurable) (measurable_dist measurableSet_Ioo)
-
-
+  exact Measurable.indicator (helper f_measurable) (measurable_dist measurableSet_Ioo)
 
 theorem CarlesonOperatorReal_mul {f : ℝ → ℂ} {x : ℝ} {a : ℝ} (ha : 0 < a) : T f x = a.toNNReal * T (fun x ↦ 1 / a * f x) x := by
   rw [CarlesonOperatorReal, CarlesonOperatorReal, ENNReal.mul_iSup]

Carleson/Theorem1_1/Carleson_on_the_real_line.lean

@@ -66,9 +66,7 @@ lemma ConditionallyCompleteLattice.le_biSup {α : Type} [ConditionallyCompleteLi
     by_cases h : z ∈ s
     · have : (@Set.range α (z ∈ s) fun _ ↦ f z) = {f z} := by
         rw [Set.eq_singleton_iff_unique_mem]
-        constructor
-        · simpa
-        · exact fun x hx => hx.2.symm
+        exact ⟨Set.mem_range_self h, fun x hx => hx.2.symm⟩
       rw [this] at hz
       have : sSup {f z} = f z := csSup_singleton _
       rw [this] at hz
@@ -85,11 +83,10 @@ lemma ConditionallyCompleteLattice.le_biSup {α : Type} [ConditionallyCompleteLi
   rw [iSup]
   convert csSup_singleton _
   rw [Set.eq_singleton_iff_unique_mem]
-  constructor
+  refine ⟨?_, fun x hx ↦ ?_⟩
   · simp
     use hi, fia
-  · intro x hx
-    simp at hx
+  · simp at hx
     rwa [hx.2] at fia
 
 --mainly have to work for the following lemmas
@@ -289,7 +286,7 @@ instance h4 : CompatibleFunctions ℝ ℝ (2 ^ 4) where
           apply abs_nonneg
       _ ≤ 2 * max r 0 * |↑f - ↑g| := by
         gcongr
-        apply le_max_left
+        exact le_max_left _ _
     norm_cast
   cdist_mono := by
     intro x₁ x₂ r R f g h
@@ -507,20 +504,13 @@ instance h5 : IsCancellative ℝ (defaultτ 4) where
     unfold instFunctionDistancesReal
     dsimp only
     rw [max_eq_left r_pos.le]
-    set L : NNReal := ⟨⨆ (x : ℝ) (y : ℝ) (_ : x ≠ y), ‖ϕ x - ϕ y‖ / dist x y, by
-            apply Real.iSup_nonneg
-            intro x
-            apply Real.iSup_nonneg
-            intro y
-            apply Real.iSup_nonneg
-            intro _
-            apply div_nonneg (norm_nonneg _) dist_nonneg⟩  with Ldef
-    set B : NNReal := ⟨⨆ y ∈ ball x r, ‖ϕ y‖, by
-            apply Real.iSup_nonneg
-            intro i
-            apply Real.iSup_nonneg
-            intro _
-            apply norm_nonneg⟩  with Bdef
+    set L : NNReal :=
+      ⟨⨆ (x : ℝ) (y : ℝ) (_ : x ≠ y), ‖ϕ x - ϕ y‖ / dist x y,
+        Real.iSup_nonneg fun x ↦ Real.iSup_nonneg fun y ↦ Real.iSup_nonneg
+        fun _ ↦ div_nonneg (norm_nonneg _) dist_nonneg⟩ with Ldef
+    set B : NNReal :=
+      ⟨⨆ y ∈ ball x r, ‖ϕ y‖, Real.iSup_nonneg fun i ↦ Real.iSup_nonneg
+        fun _ ↦ norm_nonneg _⟩  with Bdef
     calc ‖∫ (x : ℝ) in x - r..x + r, (Complex.I * (↑(f x) - ↑(g x))).exp * ϕ x‖
       _ = ‖∫ (x : ℝ) in x - r..x + r, (Complex.I * ((↑f - ↑g) : ℤ) * x).exp * ϕ x‖ := by
         congr
@@ -550,7 +540,7 @@ instance h5 : IsCancellative ℝ (defaultτ 4) where
               forall_apply_eq_imp_iff, Set.mem_setOf_eq]
             intro h
             rw [div_le_iff (dist_pos.mpr h), dist_eq_norm]
-            apply LipschitzWith.norm_sub_le hK
+            exact LipschitzWith.norm_sub_le hK _ _
           . use K
             rw [upperBounds]
             simp only [ne_eq, Set.mem_range, forall_exists_index,
@@ -559,7 +549,7 @@ instance h5 : IsCancellative ℝ (defaultτ 4) where
             apply Real.iSup_le _ NNReal.zero_le_coe
             intro h
             rw [div_le_iff (dist_pos.mpr h), dist_eq_norm]
-            apply LipschitzWith.norm_sub_le hK
+            exact LipschitzWith.norm_sub_le hK _ _
           . use K
             rw [upperBounds]
             simp only [ne_eq, Set.mem_range, forall_exists_index,
@@ -576,18 +566,16 @@ instance h5 : IsCancellative ℝ (defaultτ 4) where
           apply ConditionallyCompleteLattice.le_biSup
           . --TODO: externalize as lemma LipschitzWithOn.BddAbove or something like that?
             rw [Real.ball_eq_Ioo]
-            apply BddAbove.mono (Set.image_mono Set.Ioo_subset_Icc_self)
-            exact isCompact_Icc.bddAbove_image (continuous_norm.comp hK.continuous).continuousOn
+            exact BddAbove.mono (Set.image_mono Set.Ioo_subset_Icc_self)
+              (isCompact_Icc.bddAbove_image (continuous_norm.comp hK.continuous).continuousOn)
           use y
           rw [Real.ball_eq_Ioo]
           use hy
       _ = 2 * Real.pi * (2 * r) * (B + r * L) * (1 + 2 * r * |((↑f - ↑g) : ℤ)|)⁻¹ := by
         ring
       _ ≤ (2 ^ 4 : ℕ) * (2 * r) * iLipNorm ϕ x r * (1 + 2 * r * ↑|(↑f - ↑g : ℤ)|) ^ (- (1 / (4 : ℝ))) := by
         gcongr
-        . apply mul_nonneg
-          apply mul_nonneg (by norm_num) (by linarith)
-          apply iLipNorm_nonneg r_pos.le
+        . exact mul_nonneg (mul_nonneg (by norm_num) (by linarith)) (iLipNorm_nonneg r_pos.le)
         . norm_num
           linarith [Real.pi_le_four]
         . unfold iLipNorm
@@ -597,8 +585,7 @@ instance h5 : IsCancellative ℝ (defaultτ 4) where
         . rw [← Real.rpow_neg_one]
           apply Real.rpow_le_rpow_of_exponent_le _ (by norm_num)
           simp only [Int.cast_abs, Int.cast_sub, le_add_iff_nonneg_right]
-          apply mul_nonneg (by linarith)
-          apply abs_nonneg
+          exact mul_nonneg (by linarith) (abs_nonneg _)
 
 
 --TODO : add some Real.vol lemma
@@ -643,8 +630,6 @@ instance h6 : IsOneSidedKernel 4 K where
 /- Lemma ?-/
 lemma h3 : HasBoundedStrongType (ANCZOperator K) 2 2 volume volume (C_Ts 4) := sorry
 
-
-
 -- #check @metric_carleson
 --#check metric_carleson K (by simp) h1 h2 _ _ h3
 
@@ -654,13 +639,13 @@ local notation "T" => CarlesonOperatorReal K
 lemma CarlesonOperatorReal_le_CarlesonOperator : T ≤ CarlesonOperator K := by
   intro f x
   rw [CarlesonOperator, CarlesonOperatorReal]
-  apply iSup_le
+  refine iSup_le ?_
   intro n
   apply iSup_le
   intro r
   apply iSup_le
   intro rpos
-  apply iSup_le
+  apply iSup_le _
   intro rle1
   apply le_iSup_of_le n _
   apply le_iSup₂_of_le r 1 _