Bump mathlib

LeanAPAP.lean

@@ -1,13 +1,10 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
-import LeanAPAP.Mathlib.Algebra.BigOperators.Group.Finset
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Group.Basic
 import LeanAPAP.Mathlib.Algebra.Group.Pointwise.Finset
 import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic
-import LeanAPAP.Mathlib.Algebra.Order.BigOperators.Group.Finset
-import LeanAPAP.Mathlib.Algebra.Order.Field.Defs
 import LeanAPAP.Mathlib.Algebra.Order.Floor
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled

LeanAPAP/FiniteField.lean

@@ -1,5 +1,4 @@
 import Mathlib.FieldTheory.Finite.Basic
-import LeanAPAP.Mathlib.Algebra.Order.BigOperators.Group.Finset
 import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Cast

LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean

@@ -4,9 +4,8 @@ import Mathlib.Data.Finset.Density
 open scoped Pointwise
 
 namespace Finset
-variable {α β : Type*} [Group α] [Fintype β] [DecidableEq β] [MulAction α β]
+variable {α : Type*} [DecidableEq α] [InvolutiveInv α] [Fintype α]
 
-@[to_additive (attr := simp)]
-lemma dens_smul_finset (a : α) (s : Finset β) : (a • s).dens = s.dens := by simp [dens]
+@[to_additive (attr := simp)] lemma dens_inv (s : Finset α) : s⁻¹.dens = s.dens := by simp [dens]
 
 end Finset

LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -1,4 +1,3 @@
-import LeanAPAP.Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 namespace Real

LeanAPAP/Physics/DRC.lean

@@ -207,7 +207,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
     rw [sum_mu _ hA₁, sum_mu _ hA₂, one_mul]
   rw [div_le_iff₀ (dLpNorm_conv_pos hp₀.ne' hB hA), ← le_div_iff₀' (zero_lt_two' ℝ)]
   simp only [apply_ite NNReal.toReal, indicate_apply, NNReal.coe_one, NNReal.coe_zero, mul_boole,
-    sum_ite_mem, univ_inter, mul_div_right_comm]
+    Fintype.sum_ite_mem, mul_div_right_comm]
   calc
     ∑ x in (s p ε B₁ B₂ A)ᶜ, (μ B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p ≤
         ∑ x in (s p ε B₁ B₂ A)ᶜ,

LeanAPAP/Physics/Unbalancing.lean

@@ -149,7 +149,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       _ ≤ sqrt (∑ i in T, ν i) * sqrt (∑ i in T, ν i * |(f ^ (2 * p)) i|) :=
         (sum_sqrt_mul_sqrt_le _ (fun i ↦ ?_) fun i ↦ ?_)
       _ ≤ sqrt (∑ i in T, ν i) * sqrt (∑ i, ν i * |(f ^ (2 * p)) i|) := by
-        gcongr; exact sum_le_univ_sum_of_nonneg fun i ↦ by positivity
+        gcongr; exact T.subset_univ
       _ = sqrt (∑ i in T, ν i) * ‖f‖_[2 * ↑p, ν] ^ p := ?_
       _ ≤ _ := by gcongr; exact mod_cast hf₁
     any_goals positivity

LeanAPAP/Prereqs/FourierTransform/Compact.lean

@@ -49,7 +49,7 @@ lemma cft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : cft f ψ = ⟪ψ, f⟫
   simp_rw [dL2Inner_eq_sum, cL2Inner_eq_expect, map_expect, map_mul, starRingEnd_self_apply,
     expect_mul, mul_expect, ← expect_sum_comm, mul_mul_mul_comm _ (conj $ f _), ← sum_mul, ←
     AddChar.inv_apply_eq_conj, ← map_neg_eq_inv, ← map_add_eq_mul, AddChar.sum_apply_eq_ite]
-  simp [add_neg_eq_zero, card_univ, Fintype.card_ne_zero, NNRat.smul_def (α := ℂ)]
+  simp [add_neg_eq_zero, card_univ, Fintype.card_ne_zero, NNRat.smul_def]
 
 /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/
 @[simp] lemma dL2Norm_cft [MeasurableSpace α] [DiscreteMeasurableSpace α] (f : α → ℂ) :
@@ -62,7 +62,7 @@ lemma cft_inversion (f : α → ℂ) (a : α) : ∑ ψ, cft f ψ * ψ a = f a :=
   classical simp_rw [cft, cL2Inner_eq_expect, expect_mul, ← expect_sum_comm, mul_right_comm _ (f _),
     ← sum_mul, ← AddChar.inv_apply_eq_conj, inv_mul_eq_div, ← map_sub_eq_div,
     AddChar.sum_apply_eq_ite, sub_eq_zero, ite_mul, zero_mul, Fintype.expect_ite_eq]
-  simp [add_neg_eq_zero, card_univ, NNRat.smul_def (α := ℂ), Fintype.card_ne_zero]
+  simp [add_neg_eq_zero, card_univ, NNRat.smul_def (K := ℂ), Fintype.card_ne_zero]
 
 /-- **Fourier inversion** for the discrete Fourier transform. -/
 lemma cft_inversion' (f : α → ℂ) : ∑ ψ, cft f ψ • ⇑ψ = f := by ext; simpa using cft_inversion _ _
@@ -115,8 +115,7 @@ lemma cft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime
 
 @[simp] lemma cft_trivNChar [DecidableEq α] : cft (trivNChar : α → ℂ) = 1 := by
   ext
-  simp [trivChar_apply, cft_apply, cL2Inner_eq_expect, ← map_expect, card_univ,
-    NNRat.smul_def (α := ℂ)]
+  simp [trivChar_apply, cft_apply, cL2Inner_eq_expect, ← map_expect, card_univ, NNRat.smul_def]
 
 @[simp] lemma cft_one : cft (1 : α → ℂ) = trivChar :=
   dft_injective $ by classical rw [dft_trivChar, dft_cft, Pi.one_comp]
@@ -125,7 +124,7 @@ variable [DecidableEq α]
 
 @[simp] lemma cft_indicate_zero (s : Finset α) : cft (𝟭 s) 0 = s.dens := by
   simp only [cft_apply, cL2Inner_eq_expect, expect_indicate, AddChar.zero_apply, map_one, one_mul,
-    dens, NNRat.smul_def (α := ℂ), div_eq_inv_mul]
+    dens, NNRat.smul_def (K := ℂ), div_eq_inv_mul]
   simp
 
 lemma cft_cconv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) : cft (f ∗ₙ g) ψ = cft f ψ * cft g ψ := by

lake-manifest.json

@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "555be78e7f1df5d448c64e4282ece0dcc21214ff",
+   "rev": "09c50fb84c0b5e89b270ff20af6ae7e4bd61511e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,