last part

Carleson/Classical/CarlesonOnTheRealLine.lean

@@ -178,7 +178,7 @@ lemma coeΘ_R_C (n : Θ ℝ) (x : ℝ) : (n x : ℂ) = n * x := by norm_cast
 lemma oscillation_control {x : ℝ} {r : ℝ} {f g : Θ ℝ} :
     localOscillation (ball x r) (coeΘ f) (coeΘ g) ≤ dist_{x, r} f g := by
   by_cases r_pos : r ≤ 0
-  . rw [ball_eq_empty.mpr r_pos]
+  · rw [ball_eq_empty.mpr r_pos]
     unfold localOscillation
     simp [dist_nonneg]
   push_neg at r_pos
@@ -199,7 +199,7 @@ lemma oscillation_control {x : ℝ} {r : ℝ} {f g : Θ ℝ} :
       --TODO: investigate strange (delaborator) behavior - why is there still a sup?
       intro z
       apply Real.iSup_le
-      . intro hz
+      · intro hz
         simp at hz
         rw [Real.dist_eq, Real.dist_eq] at hz
         rw [Real.norm_eq_abs]
@@ -222,7 +222,7 @@ lemma frequency_monotone {x₁ x₂ r R : ℝ} {f g : Θ ℝ} (h : ball x₁ r 
   unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal
   dsimp
   by_cases r_pos : r ≤ 0
-  . rw [ball_eq_empty.mpr r_pos] at h
+  · rw [ball_eq_empty.mpr r_pos] at h
     rw [max_eq_right r_pos]
     gcongr
     apply le_max_right
@@ -235,21 +235,21 @@ lemma frequency_ball_doubling {x₁ x₂ r : ℝ} {f g : Θ ℝ} : dist_{x₂, 2
   unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal Real.pseudoMetricSpace
   dsimp
   by_cases r_nonneg : r ≥ 0
-  . rw [max_eq_left, max_eq_left]
+  · rw [max_eq_left, max_eq_left]
     ring_nf;rfl
     all_goals linarith [r_nonneg]
-  . rw [max_eq_right, max_eq_right]
+  · rw [max_eq_right, max_eq_right]
     simp
     all_goals linarith [r_nonneg]
 
   theorem frequency_ball_growth {x₁ x₂ r : ℝ} {f g : Θ ℝ} : 2 * dist_{x₁, r} f g ≤ dist_{x₂, 2 * r} f g := by
     unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal
     dsimp
     by_cases r_nonneg : r ≥ 0
-    . rw [max_eq_left, max_eq_left]
+    · rw [max_eq_left, max_eq_left]
       ring_nf;rfl
       all_goals linarith [r_nonneg]
-    . rw [max_eq_right, max_eq_right]
+    · rw [max_eq_right, max_eq_right]
       simp
       all_goals linarith [r_nonneg]
 
@@ -261,7 +261,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
   · --trivial case
     use {f}
     constructor
-    . norm_num
+    · norm_num
     simp only [Finset.mem_singleton, Set.iUnion_iUnion_eq_left]
     rw [Metric.ball_eq_empty.mpr R'pos, Set.subset_empty_iff, Metric.ball_eq_empty]
     linarith
@@ -270,12 +270,12 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
   · --trivial case
     use {f}
     constructor
-    . norm_num
+    · norm_num
     simp only [Finset.mem_singleton, Set.iUnion_iUnion_eq_left]
     convert Set.subset_univ _
     ext g
     constructor
-    . simp
+    · simp
     simp only [Set.mem_univ, mem_ball, true_implies]
     unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal
     dsimp
@@ -302,7 +302,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
   /- m₁, m₂, m₃ each correspond to one case. -/
   simp only [Set.mem_iUnion, mem_ball, exists_prop]
   by_cases h : φ ≤ f - R' / (2 * R)
-  . use m₁
+  · use m₁
     constructor
     · rw [balls_def]
       simp
@@ -322,15 +322,15 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
       _ = 2 * R * (m₁ - f) + 2 * R * (f - φ) := by ring
       _ < - R' + 2 * R' := by
         apply add_lt_add_of_le_of_lt
-        . rw [m₁def]
+        · rw [m₁def]
           calc 2 * R * (⌊f - R' / (2 * R)⌋ - f)
             _ ≤ 2 * R * (f - R' / (2 * R) - f) := by
               gcongr
               apply Int.floor_le
             _ = -R' := by
               ring_nf
               rw [mul_comm, ←mul_assoc, inv_mul_cancel Rpos.ne.symm, one_mul]
-        . calc 2 * R * (↑f - ↑φ)
+        · calc 2 * R * (↑f - ↑φ)
             _ ≤ 2 * R * |↑f - ↑φ| := by
               gcongr
               apply le_abs_self
@@ -346,7 +346,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
       _ = R' := by ring
   push_neg at h
   by_cases h' : φ < f + R' / (2 * R)
-  . use m₂
+  · use m₂
     constructor
     · rw [balls_def]
       simp
@@ -367,7 +367,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
   push_neg at h'
   use m₃
   constructor
-  . simp [balls_def]
+  · simp [balls_def]
   unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal
   dsimp
   push_cast
@@ -382,7 +382,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
     _ = 2 * R * (φ - f) + 2 * R * (f - m₃) := by ring
     _ < 2 * R' - R' := by
       apply add_lt_add_of_lt_of_le
-      . calc 2 * R * (↑φ - ↑f)
+      · calc 2 * R * (↑φ - ↑f)
           _ ≤ 2 * R * |↑φ - ↑f| := by
             gcongr
             exact le_abs_self _
@@ -398,7 +398,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
             symm
             rw [max_eq_left_iff]
             exact Rpos.le
-      . rw [m₃def]
+      · rw [m₃def]
         calc 2 * R * (f - ⌈f + R' / (2 * R)⌉)
           _ ≤ 2 * R * (f - (f + R' / (2 * R))) := by
             gcongr
@@ -427,8 +427,8 @@ instance compatibleFunctions_R : CompatibleFunctions ℝ ℝ (2 ^ 4) where
     unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal
     dsimp
     by_cases r_nonneg : 0 ≤ r
-    . gcongr; norm_num
-    . push_neg at r_nonneg
+    · gcongr; norm_num
+    · push_neg at r_nonneg
       rw [max_eq_right (by linarith), max_eq_right (by linarith)]
   ballsCoverBalls := by
     intro x R R' f
@@ -441,7 +441,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
   norm_integral_exp_le := by
     intro x r ϕ K hK _ f g
     by_cases r_pos : 0 ≥ r
-    . rw [ball_eq_empty.mpr r_pos]
+    · rw [ball_eq_empty.mpr r_pos]
       simp
     push_neg at r_pos
     rw [defaultτ, ← one_div, measureReal_def, Real.volume_ball, ENNReal.toReal_ofReal (by linarith [r_pos]), Real.ball_eq_Ioo, ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by linarith [r_pos])]
@@ -468,26 +468,26 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
         norm_cast
       _ ≤ 2 * Real.pi * ((x + r) - (x - r)) * (B + L * ((x + r) - (x - r)) / 2) * (1 + |((↑f - ↑g) : ℤ)| * ((x + r) - (x - r)))⁻¹ := by
         apply van_der_Corput (by linarith)
-        . rw [lipschitzWith_iff_dist_le_mul]
+        · rw [lipschitzWith_iff_dist_le_mul]
           intro x y
           --TODO: The following could be externalised as a lemma.
           by_cases hxy : x = y
-          . rw [hxy]
+          · rw [hxy]
             simp
           rw [dist_eq_norm, ← div_le_iff (dist_pos.mpr hxy), Ldef, NNReal.coe_mk]
           --apply ConditionallyCompleteLattice.le_csSup
           apply le_ciSup_of_le _ x
           apply le_ciSup_of_le _ y
           apply le_ciSup_of_le _ hxy
           rfl
-          . use K
+          · use K
             rw [upperBounds]
             simp only [ne_eq, Set.mem_range, exists_prop, and_imp,
               forall_apply_eq_imp_iff, Set.mem_setOf_eq]
             intro h
             rw [div_le_iff (dist_pos.mpr h), dist_eq_norm]
             exact LipschitzWith.norm_sub_le hK _ _
-          . use K
+          · use K
             rw [upperBounds]
             simp only [ne_eq, Set.mem_range, forall_exists_index,
               forall_apply_eq_imp_iff, Set.mem_setOf_eq]
@@ -496,7 +496,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
             intro h
             rw [div_le_iff (dist_pos.mpr h), dist_eq_norm]
             exact LipschitzWith.norm_sub_le hK _ _
-          . use K
+          · use K
             rw [upperBounds]
             simp only [ne_eq, Set.mem_range, forall_exists_index,
               forall_apply_eq_imp_iff, Set.mem_setOf_eq]
@@ -507,10 +507,10 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
             intro h
             rw [div_le_iff (dist_pos.mpr h), dist_eq_norm]
             apply LipschitzWith.norm_sub_le hK
-        . --prove main property of B
+        · --prove main property of B
           intro y hy
           apply ConditionallyCompleteLattice.le_biSup
-          . --TODO: externalize as lemma LipschitzWithOn.BddAbove or something like that?
+          · --TODO: externalize as lemma LipschitzWithOn.BddAbove or something like that?
             rw [Real.ball_eq_Ioo]
             exact BddAbove.mono (Set.image_mono Set.Ioo_subset_Icc_self)
               (isCompact_Icc.bddAbove_image (continuous_norm.comp hK.continuous).continuousOn)
@@ -521,14 +521,14 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
         ring
       _ ≤ (2 ^ 4 : ℕ) * (2 * r) * iLipNorm ϕ x r * (1 + 2 * r * ↑|(↑f - ↑g : ℤ)|) ^ (- (1 / (4 : ℝ))) := by
         gcongr
-        . exact mul_nonneg (mul_nonneg (by norm_num) (by linarith)) (iLipNorm_nonneg r_pos.le)
-        . norm_num
+        · exact mul_nonneg (mul_nonneg (by norm_num) (by linarith)) (iLipNorm_nonneg r_pos.le)
+        · norm_num
           linarith [Real.pi_le_four]
-        . unfold iLipNorm
+        · unfold iLipNorm
           gcongr
           apply le_of_eq Bdef
           apply le_of_eq Ldef
-        . rw [← Real.rpow_neg_one]
+        · 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]
           exact mul_nonneg (by linarith) (abs_nonneg _)