feat: bump to 4.16.0rc2 (#206)

I've upstreamed several things already, so this makes for a nice
cleanup.

Carleson/Classical/HilbertKernel.lean

@@ -90,7 +90,7 @@ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧
   rw [k_of_abs_le_one, k_of_abs_le_one]
   · simp only [abs_neg, ofReal_neg, mul_neg, ge_iff_le]
     rw [_root_.abs_of_nonneg yy'nonneg.1, _root_.abs_of_nonneg yy'nonneg.2]
-    let f : ℝ → ℂ := fun t ↦ (1 - t) / (1 - exp (-(I * t)))
+    set f : ℝ → ℂ := fun t ↦ (1 - t) / (1 - exp (-(I * t))) with hf
     set f' : ℝ → ℂ := fun t ↦ (-1 + exp (-(I * t)) + I * (t - 1) * exp (-(I * t))) / (1 - exp (-(I * t))) ^ 2 with f'def
     set c : ℝ → ℂ := fun t ↦ (1 - t) with cdef
     set c' : ℝ → ℂ := fun t ↦ -1 with c'def
@@ -117,7 +117,7 @@ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧
         _ > 0 := Real.sin_pos_of_pos_of_lt_pi (by linarith) (by linarith [Real.two_le_pi])
     have f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t := by
       intro t ht
-      have : f = fun t ↦ c t / d t := by simp
+      have : f = fun t ↦ c t / d t := rfl
       rw [this]
       have : f' = fun t ↦ ((c' t * d t - c t * d' t) / d t ^ 2) := by ext t; ring_nf
       rw [this]
@@ -139,7 +139,7 @@ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧
     have f'_cont : ContinuousOn (fun t ↦ f' t) (Set.uIcc y' y) :=
       ContinuousOn.div (by fun_prop) (by fun_prop) (by simpa using fun _ ht ↦ d_nonzero ht)
     calc ‖(1 - ↑y) / (1 - exp (-(I * ↑y))) - (1 - ↑y') / (1 - exp (-(I * ↑y')))‖
-      _ = ‖f y - f y'‖ := by simp
+      _ = ‖f y - f y'‖ := by simp [hf]
       _ = ‖∫ (t : ℝ) in y'..y, f' t‖ := by
         congr 1
         rw [intervalIntegral.integral_eq_sub_of_hasDerivAt]

Carleson/Discrete/Defs.lean

@@ -1,5 +1,4 @@
 import Carleson.MinLayerTiles
-import Carleson.ToMathlib.Data.Set.Finite.Lattice
 
 open MeasureTheory Measure NNReal Metric Set
 open scoped ENNReal
@@ -75,7 +74,8 @@ lemma exists_bound_ℭ : ∃ (n : ℕ × ℕ),
     ∀ x ∈ {kn : ℕ × ℕ | (ℭ (X := X) kn.1 kn.2).Nonempty}, Prod.snd x ≤ Prod.snd n := by
   apply exists_upper_bound_image
   have : Set.Finite (⋃ kn : ℕ × ℕ, ℭ (X := X) kn.1 kn.2) := toFinite _
-  exact ((Set.finite_iUnion_iff_of_pairwiseDisjoint pairwiseDisjoint_ℭ).1 this).2
+  exact ((Set.finite_iUnion_iff (fun i j hij ↦ pairwiseDisjoint_ℭ (mem_univ i) (mem_univ j) hij)).1
+    this).2
 
 variable (X) in
 def maxℭ : ℕ := (exists_bound_ℭ (X := X)).choose.2

Carleson/Discrete/SumEstimates.lean

@@ -1,4 +1,4 @@
-import Carleson.ToMathlib.Analysis.SumIntegralComparisons
+import Mathlib.Analysis.SumIntegralComparisons
 import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.Analysis.SpecialFunctions.Gamma.Basic
 import Mathlib.Data.Complex.ExponentialBounds
@@ -33,7 +33,7 @@ lemma sum_Ico_pow_mul_exp_neg_le {k : ℕ} {M : ℕ} {c : ℝ} (hc : 0 < c) :
     ∑ i ∈ Finset.Ico 0 M, i ^ k * rexp (- (c * i)) ≤ rexp c * k ! / c ^ (k + 1) := calc
   ∑ i ∈ Finset.Ico 0 M, i ^ k * rexp (- (c * i))
   _ ≤ ∫ x in (0 : ℕ).. M, x ^ k * rexp (- (c * (x - 1))) := by
-    apply sum_mul_le_integral_of_monotone_antitone
+    apply sum_mul_Ico_le_integral_of_monotone_antitone
       (f := fun x ↦ x ^ k) (g := fun x ↦ rexp (- (c * x)))
     · exact Nat.zero_le M
     · intro x hx y hy hxy

Carleson/ForestOperator/AlmostOrthogonality.lean

@@ -220,7 +220,7 @@ lemma adjointCarleson_adjoint
     _ = ∫ x, ∫ y, H x y := by unfold H; simp_rw [← integral_mul_left, mul_assoc]
     _ = ∫ y, ∫ x, H x y := integral_integral_swap hH
     _ = ∫ y, (∫ x, conj (g x) * (E p).indicator 1 x * MKD (𝔰 p) x y) * f y := by
-      simp_rw [integral_mul_right]
+      simp_rw [H, integral_mul_right]
     _ = ∫ y, conj (∫ x, g x * (E p).indicator 1 x * conj (MKD (𝔰 p) x y)) * f y := by
       simp_rw [← integral_conj]; congrm (∫ _, (∫ _, ?_) * (f _))
       rw [map_mul, conj_conj, map_mul, conj_indicator, map_one]
@@ -285,13 +285,13 @@ lemma adjoint_tree_estimate (hu : u ∈ t) (hf : BoundedCompactSupport f) :
     eLpNorm (adjointCarlesonSum (t u) f) 2 volume ≤
     C7_4_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume := by
   rw [C7_4_2_def]
-  let g := adjointCarlesonSum (t u) f
+  set g := adjointCarlesonSum (t u) f
   have hg : BoundedCompactSupport g := hf.adjointCarlesonSum
   have h := density_tree_bound1 hg hf hu
   simp_rw [adjointCarlesonSum_adjoint hg hf] at h
   have : ‖∫ x, conj (adjointCarlesonSum (t u) f x) * g x‖₊ =
       (eLpNorm g 2 volume)^2 := by
-    simp_rw [mul_comm, Complex.mul_conj]; exact _aux_L2NormSq <| hg.memℒp 2
+    simp_rw [mul_comm, g, Complex.mul_conj]; exact _aux_L2NormSq <| hg.memℒp 2
   rw [this, pow_two, mul_assoc, mul_comm _ (eLpNorm f _ _), ← mul_assoc] at h
   by_cases hgz : eLpNorm g 2 volume = 0
   · simp [hgz]

Carleson/HardyLittlewood.lean

@@ -109,15 +109,14 @@ lemma MeasureTheory.LocallyIntegrable.integrableOn_ball [ProperSpace X]
   hf.integrableOn_of_isBounded isBounded_ball
 
 -- move
-lemma MeasureTheory.LocallyIntegrable.laverage_ball_lt_top
-    [MeasurableSpace E] [BorelSpace E] [BorelSpace X] [ProperSpace X]
+lemma MeasureTheory.LocallyIntegrable.laverage_ball_lt_top [ProperSpace X]
     {f : X → E} (hf : LocallyIntegrable f μ)
     {x₀ : X} {r : ℝ} :
     ⨍⁻ x in ball x₀ r, ‖f x‖₊ ∂μ < ⊤ :=
   laverage_lt_top hf.integrableOn_ball.2.ne
 
 private lemma T.add_le [MeasurableSpace E] [BorelSpace E] [BorelSpace X] [ProperSpace X]
-    (i : ι) {f g : X → E} (hf : LocallyIntegrable f μ) (hg : LocallyIntegrable g μ) :
+    (i : ι) {f g : X → E} (hf : LocallyIntegrable f μ) :
     ‖T μ c r i (f + g)‖ₑ ≤ ‖T μ c r i f‖ₑ + ‖T μ c r i g‖ₑ := by
   simp only [T, Pi.add_apply, enorm_eq_self]
   rw [← laverage_add_left hf.integrableOn_ball.aemeasurable.ennnorm]
@@ -363,7 +362,7 @@ protected theorem MeasureTheory.AESublinearOn.maximalFunction
   · intro f c hf; rw [NNReal.smul_def]; exact hf.const_smul _
   · intro f c hf; rw [NNReal.smul_def]; exact hf.const_smul _
   · intro i _
-    refine AESublinearOn.const (T μ c r i) P (fun hf hg ↦ T.add_le i (hP hf) (hP hg))
+    refine AESublinearOn.const (T μ c r i) P (fun hf hg ↦ T.add_le i (hP hf))
       (fun f d hf ↦ T.smul i (hP hf)) |>.indicator _
 
 /-- The constant factor in the statement that `M_𝓑` has strong type. -/

Carleson/RealInterpolation.lean

@@ -2486,7 +2486,7 @@ lemma estimate_trnc {p₀ q₀ q : ℝ} {spf : ScaledPowerFunction} {j : Bool}
     (p₀⁻¹ * q₀) := by
   have := spf.hd
   unfold eLpNorm eLpNorm'
-  let tc := spf_to_tc spf
+  set tc := spf_to_tc spf
   split_ifs with is_p₀pos is_p₀top
   · have : p₀ ≤ 0 := ofReal_eq_zero.mp is_p₀pos
     contrapose! this; exact hp₀

Carleson/TileExistence.lean

@@ -1919,17 +1919,18 @@ lemma disjoint_frequency_cubes {f g : 𝓩 I} (h : (Ω₁ ⟨I, f⟩ ∩ Ω₁ 
 
 /-- Equation (4.2.6), first inclusion -/
 lemma ball_subset_Ω₁ (p : 𝔓 X) : ball_(p) (𝒬 p) C𝓩 ⊆ Ω₁ p := by
-  rw [Ω₁, Ω₁_aux]; set I := p.1; set z := p.2
-  let k := (Finite.equivFin ↑(𝓩 I)) z
-  simp_rw [Fin.eta, Equiv.symm_apply_apply, k.2, dite_true]
-  change ball_{I} z.1 C𝓩 ⊆ _ \ ⋃ i < k.1, Ω₁_aux I i
+  rw [Ω₁, Ω₁_aux]; set z := p.2
+  simp_rw [Fin.eta, Equiv.symm_apply_apply]
+  set k := (Finite.equivFin ↑(𝓩 p.1)) z with h'k
+  simp_rw [k.2, dite_true]
+  change ball_{p.1} z.1 C𝓩 ⊆ _ \ ⋃ i < k.1, Ω₁_aux p.1 i
   refine subset_diff.mpr ⟨subset_diff.mpr ⟨ball_subset_ball (by norm_num), ?_⟩, ?_⟩
   · rw [disjoint_iUnion₂_right]; intro i hi; rw [mem_diff_singleton] at hi
     exact 𝓩_pairwiseDisjoint z.coe_prop hi.1 hi.2.symm
   · rw [disjoint_iUnion₂_right]; intro i hi
-    let z' := (Finite.equivFin ↑(𝓩 I)).symm ⟨i, by omega⟩
+    let z' := (Finite.equivFin ↑(𝓩 p.1)).symm ⟨i, by omega⟩
     have zn : z ≠ z' := by simp only [ne_eq, Equiv.eq_symm_apply, z']; exact Fin.ne_of_gt hi
-    simpa [z'] using disjoint_ball_Ω₁_aux I z'.2 z.2 (Subtype.coe_ne_coe.mpr zn.symm)
+    simpa [z'] using disjoint_ball_Ω₁_aux p.1 z'.2 z.2 (Subtype.coe_ne_coe.mpr zn.symm)
 
 /-- Equation (4.2.6), second inclusion -/
 lemma Ω₁_subset_ball (p : 𝔓 X) : Ω₁ p ⊆ ball_(p) (𝒬 p) C4_2_1 := by
@@ -1944,7 +1945,7 @@ lemma Ω₁_subset_ball (p : 𝔓 X) : Ω₁ p ⊆ ball_(p) (𝒬 p) C4_2_1 := b
 /-- Equation (4.2.5) -/
 lemma iUnion_ball_subset_iUnion_Ω₁ : ⋃ z ∈ 𝓩 I, ball_{I} z C4_2_1 ⊆ ⋃ f : 𝓩 I, Ω₁ ⟨I, f⟩ := by
   rw [iUnion₂_subset_iff]; intro z mz (ϑ : Θ X) mϑ
-  let f := Finite.equivFin (𝓩 I)
+  set f := Finite.equivFin (𝓩 I) with hf
   by_cases h : ∃ y ∈ 𝓩 I, ϑ ∈ ball_{I} y C𝓩
   · obtain ⟨z', mz', hz'⟩ := h
     exact subset_iUnion_of_subset _ subset_rfl (ball_subset_Ω₁ ⟨I, ⟨z', mz'⟩⟩ hz')
@@ -1956,7 +1957,7 @@ lemma iUnion_ball_subset_iUnion_Ω₁ : ⋃ z ∈ 𝓩 I, ball_{I} z C4_2_1 ⊆
     have q : ∀ i < k, ϑ ∉ Ω₁_aux I i := by
       by_contra! h; obtain ⟨i, li, hi⟩ := h
       have := Ω₁_subset_ball ⟨I, f.symm i⟩
-      simp_rw [Ω₁, Equiv.apply_symm_apply] at this
+      simp_rw [Ω₁, ← hf, Equiv.apply_symm_apply] at this
       replace this : ϑ ∈ ball_{I} (f.symm i).1 C4_2_1 := this hi
       replace this : i ∈ L := by simp only [L, mem_setOf_eq, this]
       exact absurd (hk i this) (not_le.mpr li)

Carleson/ToMathlib/ENorm.lean

@@ -1,5 +1,4 @@
 import Mathlib.Analysis.Normed.Group.Basic
-import Mathlib.Topology.Instances.ENNReal
 import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
 
 noncomputable section

Carleson/ToMathlib/MeasureReal.lean

@@ -23,7 +23,7 @@ project, but we should probably add them back in the long run if they turn out t
 -/
 
 open MeasureTheory Measure Set symmDiff
-open scoped ENNReal NNReal
+open scoped ENNReal NNReal Function
 
 variable {ι : Type*}
 section aux_lemmas

Carleson/ToMathlib/Misc.lean

@@ -389,7 +389,8 @@ theorem indicator_const {c : ℝ} {s: Set X}
 
 end Integrable
 
--- Currently unused
+-- Currently unused.
+-- The assumption `int_f` can likely be removed, as otherwise the integral is zero.
 open Classical in
 theorem setIntegral_biUnion_le_sum_setIntegral {X : Type*} {ι : Type*} [MeasurableSpace X]
     {f : X → ℝ} (s : Finset ι) {S : ι → Set X} {μ : Measure X}
@@ -399,7 +400,7 @@ theorem setIntegral_biUnion_le_sum_setIntegral {X : Type*} {ι : Type*} [Measura
   have res_res : ∀ i ∈ s, (μ.restrict (⋃ i ∈ s, S i)).restrict (S i) = μ.restrict (S i) :=
     fun i hi ↦ by rw [Measure.restrict_restrict_of_subset]; exact (subset_biUnion_of_mem hi)
   -- Show that it suffices to prove the result in the case where the integrand is measurable
-  let g := AEMeasurable.mk f int_f.aemeasurable
+  set g := AEMeasurable.mk f int_f.aemeasurable with hg
   have g_ae_nonneg : ∀ᵐ (x : X) ∂μ.restrict (⋃ i ∈ s, S i), 0 ≤ g x := by
     apply f_ae_nonneg.congr ∘ int_f.aemeasurable.ae_eq_mk.mp
     exact Filter.Eventually.of_forall (fun _ h ↦ by rw [h])
@@ -432,7 +433,7 @@ theorem setIntegral_biUnion_le_sum_setIntegral {X : Type*} {ι : Type*} [Measura
     rw [Filter.EventuallyLE, this, Measure.ae_sum_iff' (by exact meas)]
     intro i
     by_cases hi : i ∈ s
-    · simp only [Pi.zero_apply, hi, reduceIte, μ₀, ← res_res i hi, ae_restrict_iff meas]
+    · simp only [Pi.zero_apply, hi, reduceIte, μ₀, ← res_res i hi, ae_restrict_iff meas, ← hg]
       exact g_ae_nonneg.mono (fun _ h _ ↦ h)
     · simp [hi, μ₀]