Bump mathlib

YaelDillies · Jul 31, 2024 · 04ba6a9 · 04ba6a9
1 parent cae9cdf
commit 04ba6a9
Show file tree

Hide file tree

Showing 6 changed files with 4 additions and 22 deletions.
diff --git a/LeanAPAP.lean b/LeanAPAP.lean
@@ -5,7 +5,6 @@ import LeanAPAP.Mathlib.Algebra.BigOperators.Ring
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Analysis.Complex.Circle
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.Circle
-import LeanAPAP.Mathlib.Data.Fintype.BigOperators
 import LeanAPAP.Mathlib.Data.Rat.Cast.Defs
 import LeanAPAP.Mathlib.Data.Rat.Cast.Lemmas
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup

diff --git a/LeanAPAP/Mathlib/Data/Fintype/BigOperators.lean b/LeanAPAP/Mathlib/Data/Fintype/BigOperators.lean
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@@ -6,8 +6,8 @@ open scoped NNReal ENNReal Topology
 
 variable {α E : Type*} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E]
 
-lemma snormEssSup_eq_iSup (hμ : ∀ a, μ {a} ≠ 0) (f : α → E) : snormEssSup f μ = ⨆ a, ↑‖f a‖₊ :=
+lemma eLpNormEssSup_eq_iSup (hμ : ∀ a, μ {a} ≠ 0) (f : α → E) : eLpNormEssSup f μ = ⨆ a, ↑‖f a‖₊ :=
   essSup_eq_iSup hμ _
 
-@[simp] lemma snormEssSup_count [MeasurableSingletonClass α] (f : α → E) :
-    snormEssSup f .count = ⨆ a, ↑‖f a‖₊ := essSup_count _
+@[simp] lemma eLpNormEssSup_count [MeasurableSingletonClass α] (f : α → E) :
+    eLpNormEssSup f .count = ⨆ a, ↑‖f a‖₊ := essSup_count _
diff --git a/LeanAPAP/Prereqs/Expect/Basic.lean b/LeanAPAP/Prereqs/Expect/Basic.lean
@@ -3,7 +3,6 @@ import Mathlib.Algebra.Order.Module.Rat
 import Mathlib.Analysis.RCLike.Basic
 import Mathlib.Tactic.Positivity.Finset
 import LeanAPAP.Mathlib.Algebra.Algebra.Basic
-import LeanAPAP.Mathlib.Data.Fintype.BigOperators
 
 /-!
 # Average over a finset

diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
@@ -1,5 +1,4 @@
 import Mathlib.Analysis.MeanInequalitiesPow
-import LeanAPAP.Mathlib.Data.Fintype.BigOperators
 import LeanAPAP.Prereqs.Multinomial
 
 open Finset Fintype Nat Real

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "db8dc843e42d4ce957d1919227451a23c24d7b95",
+   "rev": "09e1ab33b2621aba98326aee36572a878b092875",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,