Bump mathlib

LeanAPAP.lean

@@ -7,13 +7,11 @@ import LeanAPAP.Mathlib.Algebra.Order.Field.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Group.Abs
 import LeanAPAP.Mathlib.Algebra.Order.Group.PosPart
 import LeanAPAP.Mathlib.Analysis.InnerProductSpace.PiL2
-import LeanAPAP.Mathlib.Analysis.MeanInequalities
 import LeanAPAP.Mathlib.Analysis.NormedSpace.PiLp
 import LeanAPAP.Mathlib.Combinatorics.Additive.Energy
 import LeanAPAP.Mathlib.Data.Finset.Basic
 import LeanAPAP.Mathlib.Data.Fintype.Pi
 import LeanAPAP.Mathlib.Data.NNRat.Defs
-import LeanAPAP.Mathlib.Data.Real.Sqrt
 import LeanAPAP.Mathlib.Data.ZMod.Basic
 import LeanAPAP.Mathlib.GroupTheory.GroupAction.BigOperators
 import LeanAPAP.Mathlib.Tactic.Positivity

LeanAPAP/Extras/BSG.lean

@@ -201,8 +201,8 @@ lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K)
     ←filter_mem_eq_inter]
   refine Nat.cast_le.2 <| card_le_card ?_
   rintro ⟨a, b⟩
-  simp (config := { contextual := True }) only [not_le, mem_product, mem_inter, and_imp,
-    Prod.forall, not_lt, mem_filter, H_choice, filter_congr_decidable, and_self, true_and]
+  simp (config := { contextual := true }) only [not_le, mem_product, mem_inter, and_imp,
+    Prod.forall, not_lt, mem_filter, H_choice, filter_congr_decidable, and_self, true_and, X]
   rintro _ _ _ _ h
   -- I'd like automation to handle the rest of this
   refine h.le.trans ?_

LeanAPAP/FiniteField/Basic.lean

@@ -26,7 +26,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ :
     Nat.succ_le_iff.1 (le_mul_of_one_le_right zero_le' $ Nat.ceil_pos.2 $ curlog_pos hγ hγ₁)
   have hp' : (p⁻¹ : ℝ≥0) < 1 := inv_lt_one $ mod_cast hp
   have hp'' : (p : ℝ≥0).IsConjExponent _ := .conjExponent $ mod_cast hp
-  rw [mul_comm, ←div_div, div_le_iff (zero_lt_two' ℝ)]
+  rw [mul_comm, ← div_div, div_le_iff (zero_lt_two' ℝ)]
   calc
     _ ≤ _ := div_le_div_of_le (card G).cast_nonneg hAC
     _ = |⟪balance (μ A) ∗ balance (μ A), μ C⟫_[ℝ]| := ?_
@@ -38,22 +38,23 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ :
     _ = ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[↑(2 * ⌈γ.curlog⌉₊), const _ (card G)⁻¹] *
           γ ^ (-(p : ℝ)⁻¹) := ?_
     _ ≤ _ := mul_le_mul_of_nonneg_left ?_ $ by positivity
-  · rw [←balance_conv, balance, l2Inner_sub_left, l2Inner_const_left, expect_conv, sum_mu ℝ hA,
-      expect_mu ℝ hA, sum_mu ℝ hC, conj_trivial, one_mul, mul_one, ←mul_inv_cancel, ←mul_sub,
+  · rw [← balance_conv, balance, l2Inner_sub_left, l2Inner_const_left, expect_conv, sum_mu ℝ hA,
+      expect_mu ℝ hA, sum_mu ℝ hC, conj_trivial, one_mul, mul_one, ← mul_inv_cancel, ← mul_sub,
       abs_mul, abs_of_nonneg, mul_div_cancel_left] <;> positivity
-  · rw [lpNorm_mu hp''.symm.one_le hC, hp''.symm.coe.inv_sub_one, NNReal.coe_nat_cast, ←mul_rpow]
+  · rw [lpNorm_mu hp''.symm.one_le hC, hp''.symm.coe.inv_sub_one, NNReal.coe_nat_cast, ← mul_rpow]
     rw [le_div_iff, mul_comm] at hγC
     refine' rpow_le_rpow_of_nonpos _ hγC (neg_nonpos.2 _)
     all_goals positivity
-  · simp_rw [Nat.cast_mul, Nat.cast_two]
+  · simp_rw [Nat.cast_mul, Nat.cast_two, p]
     rw [wlpNorm_const_right, mul_assoc, mul_left_comm, NNReal.coe_inv, inv_rpow, rpow_neg]
     push_cast
     any_goals norm_cast; rw [Nat.succ_le_iff]
     rfl
     all_goals positivity
-  · push_cast
+  · dsimp [p]
+    push_cast
     norm_num
-    rw [←neg_mul, rpow_mul, one_div, rpow_inv_le_iff_of_pos]
+    rw [← neg_mul, rpow_mul, one_div, rpow_inv_le_iff_of_pos]
     refine' (rpow_le_rpow_of_exponent_ge hγ hγ₁ $ neg_le_neg $
       inv_le_inv_of_le (curlog_pos hγ hγ₁) $ Nat.le_ceil _).trans $
         (rpow_neg_inv_curlog_le hγ.le hγ₁).trans $ exp_one_lt_d9.le.trans $ by norm_num
@@ -96,12 +97,12 @@ lemma di_in_ff (hε₀ : 0 < ε) (hε₁ : ε < 1) (hαA : α ≤ A.card / card
     simp [smul_dconv, dconv_smul, smul_smul]
   · simp [card_univ, show (card G : ℂ) ≠ 0 by sorry]
   · simp only [comp_const, Nonneg.coe_inv, NNReal.coe_nat_cast]
-    rw [←ENNReal.coe_one, lpNorm_const one_ne_zero]
+    rw [← ENNReal.coe_one, lpNorm_const one_ne_zero]
     sorry
     -- simp only [Nonneg.coe_one, inv_one, rpow_one, norm_inv, norm_coe_nat,
     --   mul_inv_cancel (show (card G : ℝ) ≠ 0 by positivity)]
   · have hγ' : (1 : ℝ≥0) ≤ 2 * ⌈γ.curlog⌉₊ := sorry
     sorry
-    -- simpa [wlpNorm_nsmul hγ', ←nsmul_eq_mul, div_le_iff' (show (0 : ℝ) < card G by positivity), ←
+    -- simpa [wlpNorm_nsmul hγ', ← nsmul_eq_mul, div_le_iff' (show (0 : ℝ) < card G by positivity), ←
     --   div_div, *] using global_dichotomy hA hγC hγ hAC
   sorry

LeanAPAP/Mathlib/Algebra/BigOperators/Pi.lean

@@ -15,19 +15,19 @@ lemma filter_piFinset_card_of_mem [∀ a, DecidableEq (δ a)] (t : ∀ a, Finset
     ((piFinset t).filter fun f : ∀ a, δ a ↦ f a = x).card = ∏ b in univ.erase a, (t b).card := by
   let t' : ∀ a, Finset (δ a) := fun a' ↦
     if h : a = a' then {(@Eq.ndrec _ _ δ x _ h : δ a')} else t a'
-  have : (t' a).card = 1 := by simp
+  have : (t' a).card = 1 := by simp [t']
   have h₁ : ∏ b in univ.erase a, (t b).card = ∏ b, (t' b).card := by
     rw [←@prod_erase ℕ α _ _ univ (fun b ↦ (t' b).card) a this]
     refine' Finset.prod_congr rfl _
     intro b hb
     simp only [mem_erase, Ne.def, mem_univ, and_true_iff] at hb
-    simp only [dif_neg (Ne.symm hb)]
+    simp only [dif_neg (Ne.symm hb), t']
   have h₂ : ∏ b, (t' b).card = ∏ b, ∑ i in t' b, 1 := by simp
   rw [h₁, h₂, prod_univ_sum]
   simp only [prod_const_one, ←Finset.card_eq_sum_ones]
   congr 1
   ext f
-  simp only [mem_filter, mem_piFinset]
+  simp only [mem_filter, mem_piFinset, t']
   refine' ⟨_, fun h ↦ _⟩
   · rintro ⟨hf, rfl⟩ b
     split_ifs with h₁

LeanAPAP/Mathlib/Combinatorics/Additive/Energy.lean

@@ -30,7 +30,8 @@ lemma multiplicativeEnergy_eq_sum_sq' (s : Finset α) :
   swap
   · aesop (add simp [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left])
   · congr
-    aesop (add unsafe mul_mem_mul)
+    sorry
+    -- aesop (add unsafe mul_mem_mul)
 
 @[to_additive additiveEnergy_eq_sum_sq]
 lemma multiplicativeEnergy_eq_sum_sq [Fintype α] (s : Finset α) :
@@ -40,7 +41,8 @@ lemma multiplicativeEnergy_eq_sum_sq [Fintype α] (s : Finset α) :
   swap
   · aesop (add simp [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left])
   · congr
-    aesop
+    sorry
+    -- aesop
 
 @[to_additive card_sq_le_card_mul_additiveEnergy]
 lemma card_sq_le_card_mul_multiplicativeEnergy (s t : Finset α) :

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -195,7 +195,7 @@ lemma just_the_triangle_inequality {t : G} {a : Fin k → G} (ha : a ∈ l k m 
     rw [l, Finset.mem_filter, LProp] at ha'
     refine' ha'.2.trans_eq' _
     congr with i : 1
-    simp [sub_sub]
+    simp [sub_sub, f₂]
   have h₃ : f₂ = τ t f₁ := by
     ext i : 1
     rw [translate_apply]
@@ -383,7 +383,7 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
   norm_cast at hT
   set M : ℕ := 2 * ⌈m⌉₊
   have hM₀ : (M : ℝ≥0) ≠ 0 := by positivity
-  have hM₁ : 1 < (M : ℝ≥0) := by norm_cast; simp [← Nat.succ_le_iff]; linarith
+  have hM₁ : 1 < (M : ℝ≥0) := by norm_cast; simp [← Nat.succ_le_iff, M]; linarith
   have hM : (M : ℝ≥0).IsConjExponent _ := .conjExponent hM₁
   refine ⟨T, ?_, fun t ht ↦ ?_⟩
   · calc
@@ -402,7 +402,7 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
   have (x) :=
     calc
       (τ t (μ A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C : G → ℂ) x
-        = (F ∗ μ C) x := by simp [sub_conv]
+        = (F ∗ μ C) x := by simp [sub_conv, F]
       _ = ∑ y, F y * μ C (x - y) := conv_eq_sum_sub' ..
       _ = ∑ y, F y * μ (x +ᵥ -C) y := by simp [neg_add_eq_sub]
   rw [linftyNorm_eq_ciSup]

LeanAPAP/Physics/DRC.lean

@@ -1,5 +1,4 @@
 import LeanAPAP.Mathlib.Algebra.BigOperators.Ring
-import LeanAPAP.Mathlib.Data.Real.Sqrt
 import LeanAPAP.Prereqs.Discrete.Convolution.Norm
 import LeanAPAP.Prereqs.Discrete.LpNorm.Weighted
 
@@ -112,8 +111,8 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
       positivity
     refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) $ hg s).le, this.trans $ mul_le_of_le_one_right
       ?_ $ div_le_one_of_le ?_ ?_, this.trans $ mul_le_of_le_one_left ?_ $ div_le_one_of_le ?_ ?_⟩
-    · simp_rw [←card_smul_mu, smul_dconv, dconv_smul, l2Inner_smul_left, star_trivial, nsmul_eq_mul,
-         mul_assoc]
+    · simp_rw [A₁, A₂, g, ←card_smul_mu, smul_dconv, dconv_smul, l2Inner_smul_left, star_trivial, nsmul_eq_mul,
+        mul_assoc]
     any_goals positivity
     all_goals exact Nat.cast_le.2 $ card_mono $ inter_subset_left _ _
   rw [←sum_mul, lemma_0, nsmul_eq_mul, Nat.cast_mul, ←sum_mul, mul_right_comm, ←hgB, mul_left_comm,

LeanAPAP/Physics/Unbalancing.lean

@@ -1,7 +1,6 @@
 import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Mathlib.Algebra.Order.Field.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Group.PosPart
-import LeanAPAP.Mathlib.Data.Real.Sqrt
 import LeanAPAP.Prereqs.Discrete.Convolution.Basic
 import LeanAPAP.Prereqs.Discrete.LpNorm.Weighted
 
@@ -109,9 +108,9 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       _ = (3 / 4) ^ p * ε ^ p * ∑ i in P \ T, (ν i : ℝ) := by rw [←sum_mul, mul_comm, mul_pow]
       _ ≤ 4⁻¹ * ε ^ p * ∑ i, (ν i : ℝ) := ?_
       _ = 4⁻¹ * ε ^ p := by rw [hν₁, mul_one]
-    · simp only [mem_sdiff, mem_filter, mem_univ, true_and_iff, not_le] at hi
+    · simp only [mem_sdiff, mem_filter, mem_univ, true_and_iff, not_le, P, T] at hi
       exact mul_le_mul_of_nonneg_left (pow_le_pow_left hi.1 hi.2.le _) (by positivity)
-    · refine mul_le_mul (mul_le_mul_of_nonneg_right (le_trans (pow_le_pow_of_le_one ?_ ?_ hp) ?_) $
+    · 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
         | positivity
@@ -181,7 +180,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
         rpow_le_rpow ?_ (sum_le_sum_of_subset_of_nonneg (subset_univ _) fun i _ _ ↦ ?_) ?_
     _ = _ := by
         rw [wlpNorm_eq_sum (NNReal.coe_ne_zero.1 _)]
-        simp [NNReal.smul_def, hp'.ne']
+        simp [NNReal.smul_def, hp'.ne', p']
         dsimp
         positivity
   all_goals positivity

LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean

@@ -34,7 +34,7 @@ lemma zmodAuxAux_apply (n : ℕ) (z : ℤ) : zmodAuxAux n z = Additive.ofMul (e
 /-- The character sending `k : ZMod n` to `e ^ (2 * π * i * k / n)`. -/
 private def zmodAux (n : ℕ) : AddChar (ZMod n) circle :=
   AddChar.toMonoidHom'.symm $ AddMonoidHom.toMultiplicative'' $ ZMod.lift n ⟨zmodAuxAux n, by
-    obtain hn | hn := eq_or_ne (n : ℝ) 0 <;> simp [hn, zmodAuxAux]; rw [div_self hn]; simp⟩
+    obtain hn | hn := eq_or_ne (n : ℝ) 0 <;> simp [hn, zmodAuxAux]⟩
 
 --TODO: Heavily generalise. Yaël's attempts at generalising failed :(
 @[simp] lemma aux (n : ℕ) (h) :
@@ -165,7 +165,7 @@ lemma exists_apply_ne_zero : (∃ ψ : AddChar α ℂ, ψ a ≠ 1) ↔ a ≠ 0 :
   have h₀ := congr_fun ((complexBasis α).sum_repr f) 0
   have h₁ := congr_fun ((complexBasis α).sum_repr f) a
   simp only [complexBasis_apply, Fintype.sum_apply, Pi.smul_apply, h, smul_eq_mul, mul_one,
-    map_zero_one, if_pos rfl, if_neg ha] at h₀ h₁
+    map_zero_one, if_pos rfl, if_neg ha, f] at h₀ h₁
   exact one_ne_zero (h₁.symm.trans h₀)
 
 lemma forall_apply_eq_zero : (∀ ψ : AddChar α ℂ, ψ a = 1) ↔ a = 0 := by

LeanAPAP/Prereqs/Chang.lean

@@ -1,5 +1,5 @@
 import Mathlib.Algebra.Order.Chebyshev
-import LeanAPAP.Mathlib.Analysis.MeanInequalities
+import Mathlib.Analysis.MeanInequalities
 import LeanAPAP.Prereqs.Curlog
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.LargeSpec
@@ -39,8 +39,8 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x 
       _ ≤ ‖∑ x, f x * ∑ γ in Δ, c γ * conj (γ x)‖ := ?_
       _ ≤ ∑ x, ‖f x * ∑ γ in Δ, c γ * conj (γ x)‖ := (norm_sum_le _ _)
       _ = ∑ x, ‖f x‖ * ‖∑ γ in Δ, c γ * conj (γ x)‖ := by simp_rw [norm_mul]
-      _ ≤ _ :=
-          inner_le_weight_mul_Lp_of_nonneg _ m ?_ _ _ (fun _ ↦ norm_nonneg _) fun _ ↦ norm_nonneg _
+      _ ≤ _ := inner_le_weight_mul_Lp_of_nonneg _ (p := m) ?_ _ _ (fun _ ↦ norm_nonneg _)
+            fun _ ↦ norm_nonneg _
       _ = ‖f‖_[1] ^ (1 - (m : ℝ)⁻¹) * (∑ x, ‖f x‖ * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m) ^ (m⁻¹ : ℝ) :=
         by push_cast; simp_rw [l1Norm_eq_sum, rpow_nat_cast]
   rotate_left

LeanAPAP/Prereqs/Rudin.lean

@@ -29,10 +29,6 @@ lemma AddDissociated.randomisation (c : AddChar α ℂ → ℝ) (d : AddChar α
     _ = (𝔼 a, ∏ ψ ∈ ∅, ((d ψ * ψ a) + conj (d ψ * ψ a)) / 2) * ∏ ψ ∈ ∅ᶜ, (c ψ : ℂ) :=
         Fintype.sum_eq_single ∅ fun t ht ↦ mul_eq_zero_of_left ?_ _
     _ = _ := by simp
-  simp only [map_mul, prod_div_distrib, prod_add, prod_const, ← expect_div, expect_sum_comm,
-    div_eq_zero_iff, pow_eq_zero_iff', OfNat.ofNat_ne_zero, ne_eq, card_eq_zero, compl_eq_empty_iff,
-    false_and, or_false]
-  rw [← expect_div]
   simp only [map_mul, prod_div_distrib, prod_add, prod_const, ← expect_div, expect_sum_comm,
     div_eq_zero_iff, pow_eq_zero_iff', OfNat.ofNat_ne_zero, ne_eq, card_eq_zero, compl_eq_empty_iff,
     false_and, or_false]

lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
+   "rev": "ff9850c4726f6b9fb8d8e96980c3fcb2900be8bd",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -22,19 +22,19 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b",
+   "rev": "056ca0fa8f5585539d0b940f532d9750c3a2270f",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "16cae05860b208925f54e5581ec5fd264823440c",
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.29",
+   "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "cddd40b13751035b75906b17674492052ef80bde",
+   "rev": "2a65c8db2a3d360ab01ac149592d5b8f7813606b",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.0
+leanprover/lean4:v4.7.0-rc1