Bump to v4.16.0 (#228)

Carleson/Antichain/AntichainOperator.lean

@@ -214,9 +214,9 @@ lemma MaximalBoundAntichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤
       = ↑‖carlesonOn p f x‖₊:= by rw [Finset.sum_eq_single_of_mem p.1 p.2 hne_p]
     _ ≤ ∫⁻ (y : X), ‖cexp (I * (↑((Q x) y) - ↑((Q x) x))) * Ks (𝔰 p.1) x y * f y‖₊ := by
         rw [carlesonOn, indicator, if_pos hxE]
-        refine le_trans (ennnorm_integral_le_lintegral_ennnorm _) (lintegral_mono fun z w h ↦ ?_)
+        refine le_trans (enorm_integral_le_lintegral_enorm _) (lintegral_mono fun z w h ↦ ?_)
         simp only [nnnorm_mul, coe_mul, some_eq_coe', Nat.cast_pow, Nat.cast_ofNat,
-          zpow_neg, mul_ite, mul_zero, Ks, mul_assoc] at h ⊢
+          zpow_neg, mul_ite, mul_zero, Ks, mul_assoc, enorm_eq_nnnorm] at h ⊢
         use w
     _ ≤ ∫⁻ (y : X), ‖Ks (𝔰 p.1) x y * f y‖₊ := by
       simp only [nnnorm_mul]
@@ -348,9 +348,9 @@ lemma eLpNorm_maximal_function_le' {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain
     rw [hf_top, mul_top]
     · exact le_top
     simp only [ne_eq, ENNReal.div_eq_zero_iff, mul_eq_zero, pow_eq_zero_iff',
-    OfNat.ofNat_ne_zero, false_or, false_and, sub_eq_top_iff, two_ne_top, not_false_eq_true,
+    OfNat.ofNat_ne_zero, false_or, false_and, sub_eq_top_iff, ofNat_ne_top, not_false_eq_true,
     and_true, not_or]
-    refine ⟨?_, mul_ne_top two_ne_top (mul_ne_top (mul_ne_top two_ne_top coe_ne_top)
+    refine ⟨?_, mul_ne_top ofNat_ne_top (mul_ne_top (mul_ne_top ofNat_ne_top coe_ne_top)
       (inv_ne_top.mpr (by simp)))⟩
     rw [tsub_eq_zero_iff_le]
     exact not_le.mpr (lt_trans (by norm_cast)
@@ -401,8 +401,8 @@ lemma Dens2Antichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤·) (
     have heq : (2^2 : ℝ≥0∞) / (nnq' - 1) = 8 / (2 * nnq' - 2) := by
       have h8 : (8 : ℝ≥0∞) =  2 * 4 := by norm_cast
       have h2 : ((2 : ℝ≥0∞) * nnq' - 2) = 2 * (nnq' - 1) := by
-        rw [ENNReal.mul_sub (fun _ _ ↦ two_ne_top), mul_one]
-      rw [h8, h2, ENNReal.mul_div_mul_left _ _ two_ne_zero two_ne_top]
+        rw [ENNReal.mul_sub (fun _ _ ↦ ofNat_ne_top), mul_one]
+      rw [h8, h2, ENNReal.mul_div_mul_left _ _ two_ne_zero ofNat_ne_top]
       ring_nf
     rw [heq]
     apply ENNReal.div_le_div_right
@@ -436,7 +436,7 @@ lemma Dens2Antichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤·) (
       gcongr
       have h2 : (2 : ℝ≥0∞) ^ (107 * a ^ 3) = ‖(2 : ℝ) ^ (107 * a ^ 3)‖₊ := by
         simp only [nnnorm_pow, nnnorm_two, ENNReal.coe_pow, coe_ofNat]
-      rw [h2, ← eLpNorm_const_smul]
+      rw [h2, ← enorm_eq_nnnorm, ← eLpNorm_const_smul]
       apply eLpNorm_mono_nnnorm
       intro z
       have MB_top : MB volume (↑𝔄) 𝔠 (fun 𝔭 ↦ 8 * ↑D ^ 𝔰 𝔭) f z ≠ ⊤ := by

Carleson/Antichain/AntichainTileCount.lean

@@ -149,7 +149,7 @@ lemma stack_density (𝔄 : Finset (𝔓 X)) (ϑ : Θ X) (N : ℕ) (L : Grid X)
             simp only [𝔄'_def, Finset.mem_filter] at hp
             simp_rw [← hp.2]
           have h2a : ((2 : ℝ≥0∞) ^ a)⁻¹ = 2^(-(a : ℤ)) := by
-            rw [← zpow_natCast, ENNReal.zpow_neg two_ne_zero ENNReal.two_ne_top]
+            rw [← zpow_natCast, ENNReal.zpow_neg two_ne_zero ENNReal.ofNat_ne_top]
           rw [← ENNReal.div_le_iff, ← ENNReal.div_le_iff' (Ne.symm (NeZero.ne' (2 ^ a))),
             ENNReal.div_eq_inv_mul, h2a, dens₁]
           refine le_iSup₂_of_le p hp fun c ↦ ?_

Carleson/Antichain/TileCorrelation.lean

@@ -137,7 +137,7 @@ lemma correlation_kernel_bound (ha : 1 < a) {s₁ s₂ : ℤ} (hs₁ : s₁ ∈
             (measure_ball_ne_top x₂ (D ^ s₂))
         · simp only [ne_eq, ENNReal.div_eq_top,
           pow_eq_zero_iff', OfNat.ofNat_ne_zero, mul_eq_zero, not_false_eq_true, pow_eq_zero_iff,
-          false_or, false_and, true_and, ENNReal.pow_eq_top_iff, ENNReal.two_ne_top, or_false,
+          false_or, false_and, true_and, ENNReal.pow_eq_top_iff, ENNReal.ofNat_ne_top, or_false,
           not_or]
           exact ⟨ne_of_gt (measure_ball_pos volume x₁ (defaultD_pow_pos a s₁)),
             ne_of_gt (measure_ball_pos volume x₂ (defaultD_pow_pos a s₂))⟩

Carleson/Classical/Approximation.lean

@@ -143,7 +143,7 @@ open Topology Filter
 
 /-TODO : Assumptions might be weakened-/
 lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [ContinuousAdd β] {f : ℤ → β} {a : β} (hfa : HasSum f a) :
-    Filter.Tendsto (fun N ↦ ∑ n in Icc (-Int.ofNat ↑N) N, f n) Filter.atTop (𝓝 a) := by
+    Filter.Tendsto (fun N ↦ ∑ n ∈ Icc (-Int.ofNat ↑N) N, f n) Filter.atTop (𝓝 a) := by
   have := Filter.Tendsto.add_const (- (f 0)) hfa.nat_add_neg.tendsto_sum_nat
   simp only [add_neg_cancel_right] at this
   /- Need to start at 1 instead of zero for the base case to be true. -/

Carleson/Classical/CarlesonOperatorReal.lean

@@ -38,7 +38,7 @@ lemma annulus_measurableSet {x r R : ℝ} : MeasurableSet {y | dist x y ∈ Set.
 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
-  refine le_antisymm (le_of_forall_ge_of_dense fun c hc ↦ ?_) (biSup_mono Set.inter_subset_left)
+  refine le_antisymm (le_of_forall_lt_imp_le_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

Carleson/Classical/ControlApproximationEffect.lean

@@ -435,7 +435,7 @@ lemma partialFourierSum_bound {δ : ℝ} (hδ : 0 < δ) {g : ℝ → ℂ} (measu
       norm_cast
       gcongr
       · apply nnnorm_add_le
-      · rw [← ofReal_norm_eq_coe_nnnorm, Real.norm_of_nonneg Real.two_pi_pos.le]
+      · rw [← enorm_eq_nnnorm, ← ofReal_norm_eq_enorm, Real.norm_of_nonneg Real.two_pi_pos.le]
     _ ≤ (T g x + T (⇑conj ∘ g) x + ENNReal.ofReal (π * δ * (2 * π))) / ENNReal.ofReal (2 * π) := by
       gcongr
       · apply le_CarlesonOperatorReal intervalIntegrable_g hx
@@ -590,7 +590,7 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
           positivity
         · positivity
       _ ≤ ENNReal.ofReal (2 * π) * ‖S_ N h x‖₊ := by
-        rw [← ofReal_norm_eq_coe_nnnorm]
+        rw [← enorm_eq_nnnorm, ← ofReal_norm_eq_enorm]
         gcongr
         exact hN.le
       _ ≤ ENNReal.ofReal (2 * π) * ((T h x + T (conj ∘ h) x) / (ENNReal.ofReal (2 * π)) + ENNReal.ofReal (π * δ)) := by

Carleson/Classical/DirichletKernel.lean

@@ -12,7 +12,7 @@ open Finset Complex MeasureTheory
 noncomputable section
 
 def dirichletKernel (N : ℕ) : ℝ → ℂ :=
-  fun x ↦ ∑ n in Icc (-Int.ofNat N) N, fourier n (x : AddCircle (2 * π))
+  fun x ↦ ∑ n ∈ Icc (-Int.ofNat N) N, fourier n (x : AddCircle (2 * π))
 
 def dirichletKernel' (N : ℕ) : ℝ → ℂ :=
   fun x ↦ (exp (I * N * x) / (1 - exp (-I * x)) + exp (-I * N * x) / (1 - exp (I * x)))
@@ -64,7 +64,7 @@ lemma dirichletKernel_eq {x : ℝ} (h : cexp (I * x) ≠ 1) :
   have : (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x
       = 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 (-(N : ℤ)) N, (cexp ((n + 1 / 2) * I * ↑x) - cexp ((n - 1 / 2) * I * ↑x)) := by
+      _ = ∑ n ∈ Icc (-(N : ℤ)) N, (cexp ((n + 1 / 2) * I * ↑x) - cexp ((n - 1 / 2) * I * ↑x)) := by
         rw [dirichletKernel, mul_sum]
         congr with n
         simp [sub_mul, ← exp_add, ← exp_add]
@@ -75,8 +75,8 @@ lemma dirichletKernel_eq {x : ℝ} (h : cexp (I * x) ≠ 1) :
           congr
           rw_mod_cast [← mul_assoc, mul_comm, ← mul_assoc, inv_mul_cancel₀, one_mul]
           exact Real.pi_pos.ne.symm
-      _ = ∑ n in Icc (-(N : ℤ)) N, cexp ((n + 1 / 2) * I * ↑x)
-          - ∑ n in Icc (-(N : ℤ)) N, cexp ((n - 1 / 2) * I * ↑x) := by
+      _ = ∑ n ∈ Icc (-(N : ℤ)) N, cexp ((n + 1 / 2) * I * ↑x)
+          - ∑ n ∈ Icc (-(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,
@@ -177,21 +177,21 @@ lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {x : ℝ}
     partialFourierSum N f x =
       (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * dirichletKernel N (x - y) := by
   calc partialFourierSum N f x
-    _ = ∑ n in Icc (-(N : ℤ)) N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x := by
+    _ = ∑ n ∈ Icc (-(N : ℤ)) N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x := by
       rw [partialFourierSum]
-    _ = ∑ n in Icc (-(N : ℤ)) N, (1 / (2 * π - 0)) • ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by
+    _ = ∑ n ∈ Icc (-(N : ℤ)) N, (1 / (2 * π - 0)) • ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by
       congr 1 with n
       rw [fourierCoeffOn_eq_integral, smul_mul_assoc]
-    _ = (1 / (2 * π)) * ∑ n in Icc (-(N : ℤ)) N, ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by
+    _ = (1 / (2 * π)) * ∑ n ∈ Icc (-(N : ℤ)) N, ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by
       rw_mod_cast [← smul_sum, real_smul, sub_zero]
-    _ = (1 / (2 * π)) * ∑ n in Icc (-(N : ℤ)) N, ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n) ↑y • f y) * (fourier n) ↑x)) := by
+    _ = (1 / (2 * π)) * ∑ n ∈ Icc (-(N : ℤ)) N, ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n) ↑y • f y) * (fourier n) ↑x)) := by
       congr with n
       exact (intervalIntegral.integral_mul_const _ _).symm
-    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), ∑ n in Icc (-(N : ℤ)) N, (fourier (-n)) y • f y * (fourier n) x := by
+    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), ∑ n ∈ Icc (-(N : ℤ)) N, (fourier (-n)) y • f y * (fourier n) x := by
       rw [← intervalIntegral.integral_finset_sum]
       exact fun _ _ ↦ IntervalIntegrable.mul_const
         (h.continuousOn_mul fourier_uniformContinuous.continuous.continuousOn) _
-    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * ∑ n in Icc (-(N : ℤ)) N, (fourier (-n)) y * (fourier n) x := by
+    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * ∑ n ∈ Icc (-(N : ℤ)) N, (fourier (-n)) y * (fourier n) x := by
       congr with y
       rw [mul_sum]
       congr with n

Carleson/Classical/HilbertStrongType.lean

@@ -28,7 +28,7 @@ def modulationOperator (n : ℤ) (g : ℝ → ℂ) (x : ℝ) : ℂ :=
 /-- The approximate Hilbert transform `L_N g`, defined in (11.3.2).
 defined slightly differently. -/
 def approxHilbertTransform (n : ℕ) (g : ℝ → ℂ) (x : ℝ) : ℂ :=
-  (n : ℂ)⁻¹ * ∑ k in .Ico n (2 * n),
+  (n : ℂ)⁻¹ * ∑ k ∈ .Ico n (2 * n),
     modulationOperator (-k) (partialFourierSum k (modulationOperator k g)) x
 
 /-- The kernel `k_r(x)` defined in (11.3.11).
@@ -121,7 +121,7 @@ lemma integrable_bump_convolution {f g : ℝ → ℂ} {n : ℕ}
 
 /-- The function `L'`, defined in the Proof of Lemma 11.3.5. -/
 def dirichletApprox (n : ℕ) (x : ℝ) : ℂ :=
-  (n : ℂ)⁻¹ * ∑ k in .Ico n (2 * n), dirichletKernel k x * Complex.exp (- Complex.I * k * x)
+  (n : ℂ)⁻¹ * ∑ k ∈ .Ico n (2 * n), dirichletKernel k x * Complex.exp (- Complex.I * k * x)
 
 /-- Lemma 11.3.5, part 1. -/
 lemma continuous_dirichletApprox {n : ℕ} : Continuous (dirichletApprox n) := by

Carleson/Classical/SpectralProjectionBound.lean

@@ -24,13 +24,13 @@ lemma fourierCoeff_eq_innerProduct {T : ℝ} [hT : Fact (0 < T)] [h2 : Fact (1 
 
 noncomputable section
 def partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : ↥(Lp ℂ 2 (@haarAddCircle T hT))) : Lp ℂ p (@haarAddCircle T hT) :=
-    ∑ n in Finset.Icc (-Int.ofNat N) N, fourierCoeff f n • fourierLp p n
+    ∑ n ∈ Finset.Icc (-Int.ofNat N) N, fourierCoeff f n • fourierLp p n
 
 --TODO: add some lemma relating partialFourierSum and partialFourierSumLp
 
 
 lemma partialFourierSumL2_norm {T : ℝ} [hT : Fact (0 < T)] [h2 : Fact (1 ≤ (2 : ENNReal))] {f : ↥(Lp ℂ 2 haarAddCircle)} {N : ℕ} :
-    ‖partialFourierSumLp 2 N f‖ ^ 2 = ∑ n in Finset.Icc (-Int.ofNat N) N, ‖@fourierCoeff T hT _ _ _ f n‖ ^ 2 := by
+    ‖partialFourierSumLp 2 N f‖ ^ 2 = ∑ n ∈ Finset.Icc (-Int.ofNat N) N, ‖@fourierCoeff T hT _ _ _ f n‖ ^ 2 := by
   calc ‖partialFourierSumLp 2 N f‖ ^ 2
     _ = ‖partialFourierSumLp 2 N f‖ ^ (2 : ℝ) := by
       rw [← Real.rpow_natCast]; rfl
@@ -39,7 +39,7 @@ lemma partialFourierSumL2_norm {T : ℝ} [hT : Fact (0 < T)] [h2 : Fact (1 ≤ (
     _ = ‖∑ n ∈ Finset.Icc (-Int.ofNat N) N, fourierCoeff f n • (fourierBasis.repr (@fourierLp T hT 2 h2 n))‖ ^ (2 : ℝ) := by
       rw [partialFourierSumLp, map_sum]
       simp_rw [LinearMapClass.map_smul]
-    _ = ∑ n in Finset.Icc (-Int.ofNat N) N, ‖fourierCoeff f n‖ ^ (2 : ℝ) := by
+    _ = ∑ n ∈ Finset.Icc (-Int.ofNat N) N, ‖fourierCoeff f n‖ ^ (2 : ℝ) := by
       rw [← coe_fourierBasis]
       simp only [LinearIsometryEquiv.apply_symm_apply, lp.coeFn_smul, Pi.smul_apply, ← lp.single_smul]
       have : 2 = (2 : ENNReal).toReal := by simp
@@ -48,7 +48,7 @@ lemma partialFourierSumL2_norm {T : ℝ} [hT : Fact (0 < T)] [h2 : Fact (1 ≤ (
       refine Finset.sum_congr (by simp) fun n ↦ ?_
       simp only [smul_eq_mul, mul_one]
       congr!
-    _ = ∑ n in Finset.Icc (-Int.ofNat N) N, ‖fourierCoeff f n‖ ^ 2 := by
+    _ = ∑ n ∈ Finset.Icc (-Int.ofNat N) N, ‖fourierCoeff f n‖ ^ 2 := by
       simp_rw [← Real.rpow_natCast]; rfl
 
 lemma spectral_projection_bound_sq {T : ℝ} [hT : Fact (0 < T)] (N : ℕ) (f : Lp ℂ 2 <| @haarAddCircle T hT) :

Carleson/Classical/VanDerCorput.lean

@@ -50,7 +50,8 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
         apply this
         · intro x y
           simp only [Function.comp_apply]
-          rw [edist_eq_coe_nnnorm_sub, ← map_sub, starRingEnd_apply, nnnorm_star, ← edist_eq_coe_nnnorm_sub]
+          rw [edist_eq_enorm_sub, ← map_sub, starRingEnd_apply, enorm_eq_nnnorm, nnnorm_star,
+            ← enorm_eq_nnnorm, ← edist_eq_enorm_sub]
           exact h1 _ _
         · intro x hx
           rw [Function.comp_apply, RCLike.norm_conj]

Carleson/Defs.lean

@@ -287,7 +287,7 @@ lemma integrableOn_K_Icc [IsOpenPosMeasure (volume : Measure X)] [ProperSpace X]
     _ ≤ ∫⁻ (y : X) in {y | dist x y ∈ Icc r R},
           ENNReal.ofReal (C_K a / volume.real (ball x r)) := by
       refine setLIntegral_mono measurable_const (fun y hy ↦ ?_)
-      rw [← ENNReal.ofReal_norm]
+      rw [← ofReal_norm]
       refine ENNReal.ofReal_le_ofReal <| (norm_K_le_vol_inv x y).trans ?_
       gcongr
       · exact (C_K_pos a).le

Carleson/Discrete/ExceptionalSet.lean

@@ -71,7 +71,7 @@ lemma first_exception' : volume (G₁ : Set X) ≤ 2 ^ (- 5 : ℤ) * volume G :=
     exact mul_pos_iff.2 ⟨ENNReal.pow_pos two_pos _, measure_pos_of_superset subset_rfl hF⟩
   have K_ne_top : K ≠ ⊤ := by
     simp only [K]
-    refine (div_lt_top (mul_ne_top (pow_ne_top two_ne_top) ?_) hG).ne
+    refine (div_lt_top (mul_ne_top (pow_ne_top ofNat_ne_top) ?_) hG).ne
     exact (measure_mono (ProofData.F_subset)).trans_lt measure_ball_lt_top |>.ne
   -- Define function `r : 𝔓 X → ℝ`, with garbage value `0` for `p ∉ highDensityTiles`
   have : ∀ p ∈ highDensityTiles, ∃ r ≥ 4 * (D : ℝ) ^ 𝔰 p,
@@ -118,7 +118,7 @@ lemma first_exception' : volume (G₁ : Set X) ≤ 2 ^ (- 5 : ℤ) * volume G :=
   rw [ENNReal.div_eq_inv_mul, ← mul_one (_ * _), this]
   congr
   · have h : (2 : ℝ≥0∞) ^ (2 * a + 5) = (2 : ℝ≥0∞) ^ (2 * a + 5 : ℤ) := by norm_cast
-    rw [h, ← ENNReal.zpow_add (NeZero.ne 2) two_ne_top, add_neg_cancel_right, ← pow_mul, mul_comm 2]
+    rw [h, ← ENNReal.zpow_add (NeZero.ne 2) ofNat_ne_top, add_neg_cancel_right, ← pow_mul, mul_comm 2]
     norm_cast
   · exact ENNReal.inv_mul_cancel hG vol_G_ne_top |>.symm