chore: bump (v4.14.0-rc2) (#182)

- [x] Remove `_root_.ENNReal.inv_div` since upstreamed to Mathlib leanprover-community/mathlib4#18704 - [x] Remove `Int.floor_le_iff` since upstreamed to Mathlib leanprover-community/mathlib4#18552 - [x] Remove `dense_iff_iUnion_ball` since upstreamed to Mathlib leanprover-community/mathlib4#19294 - [x] Remove `dist_eq_of_dist_zero` since upstreamed to Mathlib leanprover-community/mathlib4#19294 - [x] Remove `IsTop.isMax_iff` since upstreamed to Mathlib leanprover-community/mathlib4#19305 - [x] Remove `Int.Icc_of_eq_sub_one` since upstreamed to Mathlib leanprover-community/mathlib4#19308 --------- Co-authored-by: grunweg <[email protected]>
fpvandoorn · Nov 21, 2024 · 0ba357e · 0ba357e
1 parent 6bc609c
commit 0ba357e
Show file tree

Hide file tree

Showing 14 changed files with 78 additions and 150 deletions.
diff --git a/Carleson/Antichain/AntichainOperator.lean b/Carleson/Antichain/AntichainOperator.lean
@@ -486,7 +486,7 @@ lemma Dens2Antichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤·) (
                   apply Nat.le_mul_of_pos_right _
                   rw [tsub_pos_iff_lt]
                   exact lt_of_lt_of_le (by linarith)
-                    (Nat.mul_le_mul_left 4 (pow_le_pow_left zero_le_four ha 2))
+                    (Nat.mul_le_mul_left 4 (pow_le_pow_left₀ zero_le_four ha 2))
                 _ = 4 * a ^ 3 - 2 * a := by
                   rw [Nat.mul_sub]
                   ring_nf

diff --git a/Carleson/Classical/Basic.lean b/Carleson/Classical/Basic.lean
@@ -208,7 +208,7 @@ lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * π +
     rw [mul_assoc]
     gcongr
     field_simp
-    rw [div_le_div_iff (by norm_num) pi_pos]
+    rw [div_le_div_iff₀ (by norm_num) pi_pos]
     linarith [pi_le_four]
   _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by
     apply lower_secant_bound' xAbs

diff --git a/Carleson/Classical/VanDerCorput.lean b/Carleson/Classical/VanDerCorput.lean
@@ -208,7 +208,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
       linarith
     _ ≤ (2 * π / (1 + n * (b - a)) * (b - a)) * (B + K * (b - a) / 2) := by
       gcongr
-      rw [mul_comm, ← mul_div_assoc, div_le_div_iff (by simpa)]
+      rw [mul_comm, ← mul_div_assoc, div_le_div_iff₀ (by simpa)]
       · calc π * (1 + n * (b - a))
           _ ≤ π * (π + n * (b - a)) := by
             gcongr

diff --git a/Carleson/Discrete/ForestUnion.lean b/Carleson/Discrete/ForestUnion.lean
@@ -400,7 +400,7 @@ lemma forest_separation (hu : u ∈ 𝔘₃ k n j) (hu' : u' ∈ 𝔘₃ k n j)
   have Cidpos : 0 < (C2_1_2 a)⁻¹ ^ d := by rw [C2_1_2]; positivity
   calc
     _ ≤ (C2_1_2 a)⁻¹ ^ (Z * (n + 1)) := by
-      refine pow_le_pow_left zero_le_two ?_ _
+      refine pow_le_pow_left₀ zero_le_two ?_ _
       nth_rw 1 [C2_1_2, ← Real.inv_rpow zero_le_two, ← Real.rpow_neg_one,
         ← Real.rpow_mul zero_le_two, neg_one_mul, neg_mul, neg_neg, ← Real.rpow_one 2]
       apply Real.rpow_le_rpow_of_exponent_le one_le_two

diff --git a/Carleson/ForestOperator/LargeSeparation.lean b/Carleson/ForestOperator/LargeSeparation.lean
@@ -166,7 +166,7 @@ lemma scales_impacting_interval (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu :
       apply Grid_subset_ball (X := X) (i := 𝓘 p)
       exact xInTile
     _ < 100 * ↑D ^ (s J + 1) := by
-      apply (div_lt_div_right zero_lt_four).mp
+      apply (div_lt_div_iff_of_pos_right zero_lt_four).mp
       ring_nf
       rewrite (config := {occs := .pos [1]}) [add_comm]
       apply lt_tsub_iff_left.mp

diff --git a/Carleson/ForestOperator/RemainingTiles.lean b/Carleson/ForestOperator/RemainingTiles.lean
@@ -87,7 +87,11 @@ lemma square_function_count (hJ : J ∈ 𝓙₆ t u₁) (s' : ℤ) :
     · rw [show (8 : ℝ≥0) = 2 ^ 3 by norm_num]
       simp only [defaultD, Nat.cast_pow, Nat.cast_ofNat, defaultA,
         ← zpow_neg, ← zpow_natCast, ← zpow_mul, ← zpow_add₀ (show (2 : ℝ≥0) ≠ 0 by norm_num)]
-      gcongr
+      -- #adaptation note(2024-11-02): this line was `gcongr`
+      -- This was probably broken by mathlib4#19626 and friends, see
+      -- https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/.2319314.20adaptations.20for.20nightly-2024-11-20
+      -- for details.
+      refine zpow_le_zpow_right₀ ?ha ?hmn
       · norm_num
       · simp only [Nat.cast_mul, Nat.cast_ofNat, Nat.cast_pow, mul_neg,
         le_add_neg_iff_add_le, ← mul_add]

diff --git a/Carleson/HardyLittlewood.lean b/Carleson/HardyLittlewood.lean
@@ -232,18 +232,18 @@ theorem Set.Countable.measure_biUnion_le_lintegral [OpensMeasurableSpace X] (h
     hB (Subtype.coe_prop i) (Subtype.coe_prop j) (Subtype.coe_ne_coe.mpr hij)
   calc
     l * μ (⋃ i ∈ 𝓑, ball (c i) (r i)) ≤ l * μ (⋃ i ∈ B, ball (c i) (2 ^ 2 * r i)) := by
-          refine l.mul_left_mono (μ.mono fun x hx ↦ ?_)
+          refine mul_left_mono (μ.mono fun x hx ↦ ?_)
           simp only [mem_iUnion, mem_ball, exists_prop] at hx
           rcases hx with ⟨i, i𝓑, hi⟩
           obtain ⟨b, bB, hb⟩ := h2B i i𝓑
           refine mem_iUnion₂.mpr ⟨b, bB, hb <| mem_ball.mpr hi⟩
     _ ≤ l * ∑' i : B, μ (ball (c i) (2 ^ 2 * r i)) :=
-          l.mul_left_mono <| measure_biUnion_le μ (h𝓑.mono hB𝓑) fun i ↦ ball (c i) (2 ^ 2 * r i)
+          mul_left_mono <| measure_biUnion_le μ (h𝓑.mono hB𝓑) fun i ↦ ball (c i) (2 ^ 2 * r i)
     _ ≤ l * ∑' i : B, A ^ 2 * μ (ball (c i) (r i)) := by
-          refine l.mul_left_mono <| ENNReal.tsum_le_tsum (fun i ↦ ?_)
+          refine mul_left_mono <| ENNReal.tsum_le_tsum (fun i ↦ ?_)
           rw [sq, sq, mul_assoc, mul_assoc]
           apply (measure_ball_two_le_same (c i) (2 * r i)).trans
-          exact ENNReal.mul_left_mono (measure_ball_two_le_same (c i) (r i))
+          exact mul_left_mono (measure_ball_two_le_same (c i) (r i))
     _ = A ^ 2 * ∑' i : B, l * μ (ball (c i) (r i)) := by
           rw [ENNReal.tsum_mul_left, ENNReal.tsum_mul_left, ← mul_assoc, ← mul_assoc, mul_comm l]
     _ ≤ A ^ 2 * ∑' i : B, ∫⁻ x in ball (c i) (r i), u x ∂μ := by

diff --git a/Carleson/Psi.lean b/Carleson/Psi.lean
@@ -229,7 +229,10 @@ private lemma sum_ψ₂ (hx : 0 < x)
   have endpts := endpoint_sub_one hD hx h
   have ne : ⌈logb D (4 * x)⌉ - 1 ≠ ⌈logb D (4 * x)⌉ := pred_ne_self _
   have : nonzeroS D x = {⌈logb D (4 * x)⌉ - 1, ⌈logb D (4 * x)⌉} := by
-    rw [nonzeroS, ← endpts]; exact Int.Icc_of_eq_sub_1 endpts
+    rw [nonzeroS, ← endpts]
+    have Icc_of_eq_add_one {a b : ℤ} (h : a + 1 = b) : Finset.Icc a b = {a, b} := by
+      subst h; exact Int.Icc_eq_pair a
+    exact Icc_of_eq_add_one (add_eq_of_eq_sub endpts)
   set s₀ := ⌈logb D (4 * x)⌉
   rw [this, Finset.sum_insert ((Finset.not_mem_singleton).2 ne), Finset.sum_singleton]
   -- Now calculate the sum
@@ -259,7 +262,7 @@ lemma mem_nonzeroS_iff {i : ℤ} {x : ℝ} (hx : 0 < x) :
     i ∈ nonzeroS D x ↔ (D ^ (-i) * x) ∈ Ioo (4 * D : ℝ)⁻¹ 2⁻¹ := by
   rw [mem_Ioo, nonzeroS, Finset.mem_Icc, Int.floor_le_iff, Int.le_ceil_iff, mul_inv_rev,
     add_comm _ 1, Real.add_lt_add_iff_left, ← lt_div_iff₀ hx, mul_comm (D : ℝ)⁻¹,
-    ← div_lt_div_iff hx (inv_pos.2 (D0 hD)), div_inv_eq_mul, ← zpow_add_one₀ ((D0 hD).ne.symm),
+    ← div_lt_div_iff₀ hx (inv_pos.2 (D0 hD)), div_inv_eq_mul, ← zpow_add_one₀ ((D0 hD).ne.symm),
     zpow_neg, ← Real.rpow_intCast, ← Real.rpow_intCast, lt_logb_iff_rpow_lt hD (four_x0 hx),
     logb_lt_iff_lt_rpow hD (mul_pos two_pos hx), ← sub_eq_neg_add, ← neg_sub i 1, ← inv_mul',
     ← inv_mul', inv_lt_inv₀ (D_pow0 hD _) (mul_pos two_pos hx), Int.cast_neg, Int.cast_sub,
@@ -406,10 +409,10 @@ private lemma div_vol_le {x y : X} {c : ℝ} (hc : c > 0) (hK : Ks s x y ≠ 0)
   have v0₂ := measure_ball_pos_nnreal x (D ^ (s - 1) / 4) (by have := D0' X; positivity)
   have v0₃ := measure_ball_pos_real x (D ^ s) (zpow_pos (D0' X) _)
   have ball_subset := ball_subset_ball (x := x) (mem_Icc.1 (dist_mem_Icc_of_Ks_ne_zero hK)).1
-  apply le_trans <| (div_le_div_left hc v0₁ v0₂).2 <|
+  apply le_trans <| (div_le_div_iff_of_pos_left hc v0₁ v0₂).2 <|
     ENNReal.toNNReal_mono (measure_ball_ne_top x _) (OuterMeasureClass.measure_mono _ ball_subset)
   dsimp only
-  rw_mod_cast [measureNNReal_val, div_le_div_iff (by exact_mod_cast v0₂) v0₃]
+  rw_mod_cast [measureNNReal_val, div_le_div_iff₀ (by exact_mod_cast v0₂) v0₃]
   apply le_of_le_of_eq <| (mul_le_mul_left hc).2 <|
     DoublingMeasure.volume_ball_two_le_same_repeat' s x
   simp_rw [defaultA, ← mul_assoc, mul_comm c]
@@ -599,11 +602,11 @@ private lemma norm_Ks_sub_Ks_le₁ {s : ℤ} {x y y' : X} (hK : Ks s x y ≠ 0)
   apply le_trans <| norm_sub_le (Ks s x y) (Ks s x y')
   apply le_trans <| add_le_add norm_Ks_le norm_Ks_le
   rw [div_mul_eq_mul_div, div_add_div_same, ← two_mul,
-    div_le_div_right (measure_ball_pos_real x (D ^ s) (D_pow0' (D1 X) s)), ← pow_one 2]
+    div_le_div_iff_of_pos_right (measure_ball_pos_real x (D ^ s) (D_pow0' (D1 X) s)), ← pow_one 2]
   rw [not_le, ← div_lt_iff₀' two_pos] at h
   have dist_pos : dist y y' > 0 := lt_of_le_of_lt (div_nonneg dist_nonneg two_pos.le) h
   have := lt_of_le_of_lt
-    ((div_le_div_right two_pos).2 ((mem_Icc.1 <| dist_mem_Icc_of_Ks_ne_zero hK).1)) h
+    ((div_le_div_iff_of_pos_right two_pos).2 ((mem_Icc.1 <| dist_mem_Icc_of_Ks_ne_zero hK).1)) h
   rw [div_div, (show (4 : ℝ) * 2 = 8 by norm_num), zpow_sub₀ (D0' X).ne.symm, div_div, zpow_one,
     div_lt_comm₀ (by positivity) dist_pos] at this
   have dist_div_Ds_gt := inv_strictAnti₀ (div_pos (Ds0 X s) dist_pos) this