Bump mathlib

LeanAPAP/Extras/BSG.lean

@@ -226,7 +226,7 @@ lemma test_case {E A B : ℕ} {K : ℝ} (hK : 0 < K) (hE : K⁻¹ * (A ^ 2 * B)
     (hA : 0 < A) (hB : 0 < B) :
     A / (Real.sqrt 2 * K) ≤ Real.sqrt 2⁻¹ * (E / (A * B)) := by
   rw [inv_mul_le_iff₀ hK] at hE
-  rw [mul_div_assoc', div_le_div_iff, ← mul_assoc, ← sq]
+  rw [mul_div_assoc', div_le_div_iff₀, ← mul_assoc, ← sq]
   rotate_left
   · positivity
   · positivity
@@ -251,7 +251,7 @@ lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K) (hE : K⁻¹ * (#A ^ 2 * #
     refine this.trans' ?_
     -- I'd like automation to handle the rest of this
     rw [inv_mul_le_iff₀ hK] at hE
-    rw [mul_div_assoc', div_le_div_iff, ← mul_assoc, ← sq]
+    rw [mul_div_assoc', div_le_div_iff₀, ← mul_assoc, ← sq]
     rotate_left
     · positivity
     · positivity

LeanAPAP/FiniteField.lean

@@ -229,7 +229,7 @@ lemma ap_in_ff' (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (h
           |∑ x ∈ S, (μ (Set.toFinset V) ∗ μ A₁ ○ μ A₂) x - ∑ x ∈ S, (μ A₁ ○ μ A₂) x| ≤ ε := by
   simpa [← conjneg_mu] using ap_in_ff (q := q) S (A₂ := -A₂) hα₀ hα₂ hε₀ hε₁ hαA₁ (by simpa)
 
-set_option maxHeartbeats 300000 in
+set_option maxHeartbeats 400000 in
 lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q) (hq : q.Prime)
     (hε₀ : 0 < ε) (hε₁ : ε < 1) (hγC : γ ≤ C.dens) (hγ : 0 < γ)
     (hAC : ε ≤ |card G * ⟪μ_[ℝ] A ∗ μ A, μ C⟫_[ℝ] - 1|) :
@@ -406,7 +406,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
           wInner_one_dconv_eq_conv_wInner_one, ← dconv_wInner_one_eq_wInner_one_conv,
           ← conj_wInner_symm]
         simp [wInner_one_eq_sum, inner_apply, smul_sum, mul_assoc]
-      _ ≤ card G • (‖μ_[ℝ] (Set.toFinset V) ∗ μ A‖_[∞] * ‖μ A ∗ μ A₂ ○ μ A₁‖_[1]) := by
+      _ ≤ card G • (‖μ_[ℝ] (Set.toFinset V) ∗ μ A‖_[∞] * ‖μ_[ℝ] A ∗ μ A₂ ○ μ A₁‖_[1]) := by
         gcongr; exact wInner_one_le_dLpNorm_mul_dLpNorm .top_one _ _
       _ = _ := by
         have : 0 < (4 : ℝ)⁻¹ * A.dens ^ (2 * q') := by positivity

LeanAPAP/Mathlib/Probability/UniformOn.lean

@@ -4,7 +4,5 @@ namespace ProbabilityTheory
 variable {Ω : Type*} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω}
 
 @[simp] lemma uniformOn_eq_zero : uniformOn s = 0 ↔ s.Infinite ∨ s = ∅ := by simp [uniformOn]
-@[simp] lemma uniformOn_eq_zero' (hs : s.Finite) : uniformOn s = 0 ↔ s = ∅ := by
-  simp [uniformOn, hs]
 
 end ProbabilityTheory

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -109,22 +109,16 @@ lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hk : 64 * m / ε ^ 2 ≤ k) :
   rw [mul_pow (2 : ℝ), ← hmeq, ← dLpNorm_pow_eq_sum_norm hm' f, ← mul_assoc, ← mul_assoc,
     mul_right_comm _ (#A ^ k : ℝ), mul_right_comm _ (#A ^ k : ℝ),
     mul_right_comm _ (#A ^ k : ℝ)]
+  rw [div_le_iff₀' (by positivity)] at hk
   gcongr ?_ * _ * _
-  rw [mul_assoc (_ ^ m : ℝ), ← pow_succ, Nat.sub_add_cancel hm, pow_mul, pow_mul, ← mul_pow,
-    ← mul_pow]
-  have : (1 / 2 : ℝ) ^ m ≤ 1 / 2 := by
-    have :=
-      pow_le_pow_of_le_one (show (0 : ℝ) ≤ 1 / 2 by norm_num) (show (1 / 2 : ℝ) ≤ 1 by norm_num) hm
-    rwa [pow_one] at this
-  refine (mul_le_mul_of_nonneg_right this (by positivity)).trans' ?_
-  rw [← mul_pow]
-  refine pow_le_pow_left (by positivity) ?_ _
-  rw [mul_right_comm, mul_comm _ ε, mul_pow, ← mul_assoc, sq (k : ℝ), ← mul_assoc]
-  refine mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg k)
-  rw [mul_right_comm, div_mul_eq_mul_div, one_mul, div_mul_eq_mul_div, le_div_iff₀' (zero_lt_two' ℝ),
-    ← div_le_iff₀', ← mul_assoc]
-  · norm_num1; exact hk
-  positivity
+  calc
+    (8 * m : ℝ) ^ m * k ^ (m - 1) * k * 2 ^ (2 * m)
+      = (8 * m) ^ m * 2 ^ (2 * m) * (k ^ (m - 1) * k) := by ring
+    _ = (64 * m * k / 2) ^ m := by rw [pow_sub_one_mul (by omega), pow_mul, ← mul_pow]; ring
+    _ ≤ (ε ^ 2 * k * k / 2) ^ m := by gcongr
+    _ = (k * ε) ^ (2 * m) / 2 ^ m := by ring_nf
+    _ ≤ (k * ε) ^ (2 * m) / 2 ^ 1 := by gcongr; norm_num
+    _ = 1 / 2 * (k * ε) ^ (2 * m) := by ring
 
 end
 
@@ -353,32 +347,27 @@ lemma T_bound (hK₂ : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ)
     rw [hk, div_pow, div_div_eq_mul_div, mul_right_comm]
     congr 3
     norm_num
-  have hK : 0 < K := by positivity
+  have hK₀ : 0 < K := by positivity
   have : (0 : ℝ) < Ac ^ k := by positivity
   refine le_of_mul_le_mul_left ?_ this
-  have : (Ac : ℝ) ^ k ≤ K * Lc := by
-    rw [div_le_iff₀'] at h₂
-    refine h₂.trans (mul_le_mul_of_nonneg_right hK₂ (Nat.cast_nonneg _))
-    exact zero_lt_two
-  rw [neg_mul, neg_div, Real.rpow_neg hK.le, mul_left_comm,
-    inv_mul_le_iff₀ (Real.rpow_pos_of_pos hK _)]
-  refine (mul_le_mul_of_nonneg_right this (Nat.cast_nonneg _)).trans ?_
-  rw [mul_assoc]
-  rw [← @Nat.cast_le ℝ, Nat.cast_mul] at h₁
-  refine (mul_le_mul_of_nonneg_left h₁ hK.le).trans ?_
-  rw [Nat.cast_mul, ← mul_assoc, ← mul_assoc, Nat.cast_pow]
-  refine mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg _)
-  refine (mul_le_mul_of_nonneg_left (pow_le_pow_left (Nat.cast_nonneg _) h₃ k) hK.le).trans ?_
-  rw [mul_pow, ← mul_assoc, ← pow_succ']
-  refine mul_le_mul_of_nonneg_right ?_ (pow_nonneg (Nat.cast_nonneg _) _)
-  rw [← Real.rpow_natCast]
-  refine Real.rpow_le_rpow_of_exponent_le (one_le_two.trans hK₂) ?_
-  rw [Nat.cast_add_one, ← le_sub_iff_add_le, hk']
-  refine (Nat.ceil_lt_add_one ?_).le.trans ?_
-  · positivity
-  have : (1 : ℝ) ≤ 128 * (m / ε ^ 2) := by rw [div_eq_mul_one_div]; bound
-  rw [mul_div_assoc, mul_div_assoc]
-  linarith only [this]
+  rw [neg_mul, neg_div, Real.rpow_neg hK₀.le, mul_left_comm, inv_mul_le_iff₀ (by positivity)]
+  calc
+    (Ac ^ k * Sc : ℝ)
+      = 2 * (Ac ^ k / 2) * Sc := by ring
+    _ ≤ K * Lc * Sc := by gcongr
+    _ = K * ↑(Lc * Sc) := by push_cast; ring
+    _ ≤ K * ↑(ASc ^ k * Tc) := by gcongr
+    _ = K * ASc ^ k * Tc := by push_cast; ring
+    _ ≤ K * (K * Ac) ^ k * Tc := by gcongr
+    _ = K ^ (k + 1 : ℝ) * Ac ^ k * Tc := by norm_cast; push_cast; ring
+    _ ≤ K ^ (512 * m / ε ^ 2) * Ac ^ k * Tc := ?_
+    _ = K ^ (512 * m / ε ^ 2) * (Ac ^ k * Tc) := by ring
+  gcongr
+  · linarith
+  rw [← le_sub_iff_add_le, hk', mul_div_assoc, mul_div_assoc]
+  have h₄ := Nat.ceil_lt_add_one (a := 256 * (m / ε ^ 2)) (by positivity)
+  have h₅ : (1 : ℝ) ≤ 128 * (m / ε ^ 2) := by rw [div_eq_mul_one_div]; bound
+  linear_combination h₄ + 2 * h₅
 
 -- trivially true for other reasons for big ε
 lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (f : G → ℂ)
@@ -440,7 +429,7 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
           gcongr
           · exact one_le_two.trans hK₂
           calc
-            _ ≤ 2.7182818286 ^ 2 := pow_le_pow_left (by positivity) exp_one_lt_d9.le _
+            _ ≤ (2.7182818286 : ℝ) ^ 2 := by gcongr; exact exp_one_lt_d9.le
             _ ≤ _ := by norm_num
       _ = _ := by simp [div_div_eq_mul_div, ← mul_div_right_comm, mul_right_comm, div_pow]
       _ ≤ _ := hKT

LeanAPAP/Physics/DRC.lean

@@ -230,7 +230,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
       nnnorm_of_nonneg (this _), NNReal.coe_sum, sum_mul, mul_pow]
     simp
   calc
-    (1 - ε) ^ p ≤ exp (-ε) ^ p := pow_le_pow_left (sub_nonneg.2 hε₁) (one_sub_le_exp_neg _) _
+    (1 - ε) ^ p ≤ exp (-ε) ^ p := by gcongr; exacts [sub_nonneg.2 hε₁, one_sub_le_exp_neg _]
     _ = exp (-(ε * p)) := by rw [← neg_mul, exp_mul, rpow_natCast]
     _ ≤ exp (-log (2 / δ)) :=
       (exp_monotone $ neg_le_neg $ (inv_mul_le_iff₀ $ by positivity).1 hpε)
@@ -249,7 +249,7 @@ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p
       (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤
         4⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ univ] ^ (2 * p) / #A ^ (2 * p) := by
       rw [mul_div_assoc, ← div_pow]
-      refine mul_le_mul_of_nonneg_left (pow_le_pow_left (by positivity) ?_ _) (by norm_num)
+      gcongr
       rw [nnratCast_dens, le_div_iff₀, ← mul_div_right_comm]
       calc
         _ = (‖𝟭_[ℝ] A ○ 𝟭 A‖_[1, μ univ] : ℝ) := by

LeanAPAP/Physics/Unbalancing.lean

@@ -119,7 +119,9 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       _ ≤ 4⁻¹ * ε ^ p * ∑ i, (ν i : ℝ) := ?_
       _ = 4⁻¹ * ε ^ p := by norm_cast; simp [hν₁]
     · simp only [mem_sdiff, mem_filter, mem_univ, true_and, not_le, P, T] at hi
-      exact mul_le_mul_of_nonneg_left (pow_le_pow_left hi.1 hi.2.le _) (by positivity)
+      cases hi
+      dsimp
+      gcongr
     · refine mul_le_mul (mul_le_mul_of_nonneg_right (le_trans (pow_le_pow_of_le_one ?_ ?_ hp) ?_)
         ?_) (sum_le_univ_sum_of_nonneg fun i ↦ ?_) ?_ ?_ <;>
         first
@@ -171,7 +173,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       all_goals positivity
     any_goals positivity
     calc
-      _ ≤ (1 / 3 : ℝ) ^ p := pow_le_pow_left ?_ (div_le_div_of_nonneg_right hε₁ ?_) _
+      _ ≤ (1 / 3 : ℝ) ^ p := by gcongr
       _ ≤ (1 / 3) ^ 5 := pow_le_pow_of_le_one ?_ ?_ hp
       _ ≤ _ := ?_
     any_goals positivity

LeanAPAP/Prereqs/Chang.lean

@@ -112,7 +112,7 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x 
     exact le_abs_self _
   · norm_cast
     exact hm.bot_lt
-  replace this := pow_le_pow_left (by positivity) this m
+  replace this := pow_le_pow_left₀ (by positivity) this m
   simp_rw [mul_pow] at this
   rw [rpow_inv_natCast_pow _ hm, ← rpow_mul_natCast, one_sub_mul,
     inv_mul_cancel₀, ← Nat.cast_pred, rpow_natCast, mul_assoc, mul_left_comm, ← pow_sub_one_mul,
@@ -126,9 +126,10 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x 
         hfν _ hfx
   replace this :=
     calc
-      _ ≤ (∑ x, ‖f x‖ * sqrt (ν x) * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m) ^ 2 :=
-          pow_le_pow_left (by positivity)
-            (this.trans $ sum_le_sum fun x _ ↦ mul_le_mul_of_nonneg_right (hfν _) $ by positivity) _
+      (‖f‖_[1] * (η ^ m * #Δ ^ m)) ^ 2
+        ≤ (∑ x, ‖f x‖ * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ 2 := by gcongr
+      _ ≤ (∑ x, ‖f x‖ * sqrt (ν x) * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m) ^ 2 := by
+        gcongr with x; exact hfν _
       _ = (∑ x, ‖f x‖ * (sqrt (ν x) * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m)) ^ 2 := by
         simp_rw [mul_assoc]
       _ ≤ (∑ x, ‖f x‖ ^ 2) * ∑ x, (sqrt (ν x) * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m) ^ 2 :=
@@ -182,7 +183,7 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) :
   push_cast
   rw [← mul_assoc, ← pow_add, ← two_mul]
   refine ((spec_hoelder hη.le hΔη hβ.ne').trans $ hΔ.boringEnergy_le _).trans ?_
-  refine le_trans ?_ $ mul_le_mul_of_nonneg_right (pow_le_pow_left ?_ (Nat.le_ceil _) _) ?_
+  refine le_trans ?_ $ mul_le_mul_of_nonneg_right (pow_le_pow_left₀ ?_ (Nat.le_ceil _) _) ?_
   rw [mul_right_comm, div_pow, mul_pow, mul_pow, exp_one_pow, ← pow_mul, mul_div_assoc]
   calc
     _ = (changConst * #Δ * β) ^ β := by ring

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b100ff2565805e9f30a482788b3fc66937a7f38a",
+   "rev": "485efbc439ee0ebdeae8afb0acd24a5e82e2f771",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b0b73e5bc33f1bc4d3c0f254630dd0e262cecc08",
+   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "59e75948eb18b0946b93c99d666844ca885675c6",
+   "rev": "fb23240e8b4409f2f23bcd07aa73c7451f216413",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
+   "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7b6a56e8e4fcf54d3834b225b9814a7c9e4d4bda",
+   "rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",