From 471cd1820cb1cafcdaccf2ff6a5886c7f40a6a98 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 28 Aug 2024 12:42:09 +0000 Subject: [PATCH] Bump mathlib --- LeanAPAP.lean | 2 -- LeanAPAP/Extras/BSG.lean | 1 + LeanAPAP/FiniteField/Basic.lean | 2 +- .../SpecialFunctions/Complex/CircleAddChar.lean | 4 +++- .../Analysis/SpecialFunctions/Pow/NNReal.lean | 1 - .../Analysis/SpecialFunctions/Pow/Real.lean | 16 ---------------- .../MeasureTheory/Function/LpSeminorm/Basic.lean | 1 - .../MeasureTheory/Measure/Typeclasses.lean | 14 -------------- LeanAPAP/Physics/AlmostPeriodicity.lean | 2 +- LeanAPAP/Physics/DRC.lean | 3 +++ LeanAPAP/Physics/Unbalancing.lean | 2 +- LeanAPAP/Prereqs/Convolution/Compact.lean | 3 ++- LeanAPAP/Prereqs/Convolution/Norm.lean | 4 ++-- LeanAPAP/Prereqs/Convolution/Order.lean | 2 +- LeanAPAP/Prereqs/Convolution/ThreeAP.lean | 5 ++++- LeanAPAP/Prereqs/Convolution/WithConv.lean | 2 +- LeanAPAP/Prereqs/Energy.lean | 5 +++-- LeanAPAP/Prereqs/FourierTransform/Compact.lean | 3 ++- lake-manifest.json | 2 +- 19 files changed, 26 insertions(+), 48 deletions(-) delete mode 100644 LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean delete mode 100644 LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index 303e72e431..08686ed50f 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -5,14 +5,12 @@ import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic import LeanAPAP.Mathlib.Analysis.RCLike.Basic import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal -import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real import LeanAPAP.Mathlib.Data.ENNReal.Real import LeanAPAP.Mathlib.Data.Fintype.Order import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic import LeanAPAP.Mathlib.MeasureTheory.MeasurableSpace.Defs import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef -import LeanAPAP.Mathlib.MeasureTheory.Measure.Typeclasses import LeanAPAP.Mathlib.Order.Filter.Basic import LeanAPAP.Mathlib.Order.LiminfLimsup import LeanAPAP.Mathlib.Tactic.Positivity diff --git a/LeanAPAP/Extras/BSG.lean b/LeanAPAP/Extras/BSG.lean index a4959905df..7ede410bd5 100644 --- a/LeanAPAP/Extras/BSG.lean +++ b/LeanAPAP/Extras/BSG.lean @@ -1,5 +1,6 @@ import Mathlib.Combinatorics.Additive.Energy import Mathlib.Data.Real.StarOrdered +import LeanAPAP.Prereqs.Convolution.Discrete.Basic import LeanAPAP.Prereqs.Convolution.Order open BigOperators Finset diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean index 45cb32dc70..3aae2650f0 100644 --- a/LeanAPAP/FiniteField/Basic.lean +++ b/LeanAPAP/FiniteField/Basic.lean @@ -1,5 +1,5 @@ +import Mathlib.FieldTheory.Finite.Basic import LeanAPAP.Prereqs.Convolution.ThreeAP -import LeanAPAP.Prereqs.FourierTransform.Compact import LeanAPAP.Prereqs.LargeSpec import LeanAPAP.Physics.AlmostPeriodicity import LeanAPAP.Physics.Unbalancing diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean index 911405ccab..c7d8182a2c 100644 --- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean +++ b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean @@ -1,4 +1,6 @@ -import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar +import Mathlib.Algebra.EuclideanDomain.Basic +import Mathlib.Algebra.EuclideanDomain.Field +import Mathlib.Analysis.SpecialFunctions.Complex.Circle open AddChar Multiplicative Real open scoped ComplexConjugate Real diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean index 42d018691d..20004ebe35 100644 --- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean +++ b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean @@ -1,5 +1,4 @@ import Mathlib.Analysis.SpecialFunctions.Pow.NNReal -import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real /-! # TODO diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean deleted file mode 100644 index 901df46926..0000000000 --- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean +++ /dev/null @@ -1,16 +0,0 @@ -import Mathlib.Analysis.SpecialFunctions.Pow.Real - -namespace Real -variable {x y z : ℝ} - --- TODO: Replace in mathlib -alias rpow_add_intCast := rpow_add_int -alias rpow_add_natCast := rpow_add_nat -alias rpow_sub_intCast := rpow_sub_int -alias rpow_sub_natCast := rpow_sub_nat -alias rpow_add_intCast' := rpow_add_int' -alias rpow_add_natCast' := rpow_add_nat' -alias rpow_sub_intCast' := rpow_sub_int' -alias rpow_sub_natCast' := rpow_sub_nat' - -end Real diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean index 93fa959365..44f27cc0b2 100644 --- a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean +++ b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean @@ -1,5 +1,4 @@ import Mathlib.MeasureTheory.Function.LpSeminorm.Basic -import LeanAPAP.Mathlib.Data.ENNReal.Real noncomputable section diff --git a/LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean deleted file mode 100644 index 5c9550a3e7..0000000000 --- a/LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean +++ /dev/null @@ -1,14 +0,0 @@ -import Mathlib.MeasureTheory.Measure.Typeclasses - -namespace MeasureTheory -variable {ι α : Type*} {mα : MeasurableSpace α} {s : Finset ι} {μ : ι → Measure α} - [∀ i, IsFiniteMeasure (μ i)] - -attribute [simp] ENNReal.sum_lt_top - -instance : IsFiniteMeasure (∑ i ∈ s, μ i) where measure_univ_lt_top := by simp [measure_lt_top] - -instance [Fintype ι] : IsFiniteMeasure (.sum μ) where - measure_univ_lt_top := by simp [measure_lt_top] - -end MeasureTheory diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index e0a1f5e53b..ec36585ebb 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -1,7 +1,7 @@ import Mathlib.Algebra.Order.Chebyshev import Mathlib.Combinatorics.Additive.DoublingConst -import Mathlib.Combinatorics.Pigeonhole import Mathlib.Data.Complex.ExponentialBounds +import LeanAPAP.Prereqs.Convolution.Discrete.Basic import LeanAPAP.Prereqs.Convolution.Norm import LeanAPAP.Prereqs.Curlog import LeanAPAP.Prereqs.MarcinkiewiczZygmund diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index 479c196a8f..4677ab14f3 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/LeanAPAP/Physics/DRC.lean @@ -1,4 +1,7 @@ +import LeanAPAP.Prereqs.Convolution.Discrete.Basic import LeanAPAP.Prereqs.Convolution.Norm +import LeanAPAP.Prereqs.Convolution.Order +import LeanAPAP.Prereqs.Function.Indicator.Basic import LeanAPAP.Prereqs.LpNorm.Weighted /-! diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index 2867d48e32..3936a82760 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/LeanAPAP/Physics/Unbalancing.lean @@ -1,6 +1,6 @@ import Mathlib.Algebra.Order.Group.PosPart import Mathlib.Data.Complex.ExponentialBounds -import LeanAPAP.Prereqs.Convolution.Discrete.Basic +import LeanAPAP.Prereqs.Convolution.Discrete.Defs import LeanAPAP.Prereqs.LpNorm.Weighted /-! diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean index 7b39e694fe..85054e684e 100644 --- a/LeanAPAP/Prereqs/Convolution/Compact.lean +++ b/LeanAPAP/Prereqs/Convolution/Compact.lean @@ -1,5 +1,6 @@ -import LeanAPAP.Prereqs.Convolution.Discrete.Basic +import LeanAPAP.Prereqs.Convolution.Discrete.Defs import LeanAPAP.Prereqs.Expect.Complex +import LeanAPAP.Prereqs.Function.Indicator.Defs /-! # Convolution in the compact normalisation diff --git a/LeanAPAP/Prereqs/Convolution/Norm.lean b/LeanAPAP/Prereqs/Convolution/Norm.lean index bedd81a968..cb1d8f979d 100644 --- a/LeanAPAP/Prereqs/Convolution/Norm.lean +++ b/LeanAPAP/Prereqs/Convolution/Norm.lean @@ -1,6 +1,6 @@ import Mathlib.Data.Real.StarOrdered -import LeanAPAP.Prereqs.Convolution.Order -import LeanAPAP.Prereqs.LpNorm.Compact +import LeanAPAP.Prereqs.Convolution.Discrete.Defs +import LeanAPAP.Prereqs.LpNorm.Discrete.Basic /-! # Norm of a convolution diff --git a/LeanAPAP/Prereqs/Convolution/Order.lean b/LeanAPAP/Prereqs/Convolution/Order.lean index 68ff0fc2bb..8cf955aa8c 100644 --- a/LeanAPAP/Prereqs/Convolution/Order.lean +++ b/LeanAPAP/Prereqs/Convolution/Order.lean @@ -1,5 +1,5 @@ import LeanAPAP.Mathlib.Tactic.Positivity -import LeanAPAP.Prereqs.Convolution.Discrete.Basic +import LeanAPAP.Prereqs.Convolution.Discrete.Defs open Finset Function Real open scoped ComplexConjugate NNReal Pointwise diff --git a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean index d7d29814f8..a6badb143d 100644 --- a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean +++ b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean @@ -1,5 +1,8 @@ import Mathlib.Combinatorics.Additive.AP.Three.Defs -import LeanAPAP.Prereqs.Convolution.Norm +import Mathlib.Data.Real.StarOrdered +import LeanAPAP.Prereqs.Convolution.Discrete.Defs +import LeanAPAP.Prereqs.Function.Indicator.Defs +import LeanAPAP.Prereqs.LpNorm.Discrete.Defs /-! # The convolution characterisation of 3AP-free sets diff --git a/LeanAPAP/Prereqs/Convolution/WithConv.lean b/LeanAPAP/Prereqs/Convolution/WithConv.lean index aa25146320..54240e28e2 100644 --- a/LeanAPAP/Prereqs/Convolution/WithConv.lean +++ b/LeanAPAP/Prereqs/Convolution/WithConv.lean @@ -1,4 +1,4 @@ -import LeanAPAP.Prereqs.Convolution.Discrete.Basic +import LeanAPAP.Prereqs.Convolution.Discrete.Defs /-! # The ring of functions under convolution diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean index f8acf1446f..eab58479f7 100644 --- a/LeanAPAP/Prereqs/Energy.lean +++ b/LeanAPAP/Prereqs/Energy.lean @@ -1,6 +1,7 @@ import LeanAPAP.Prereqs.AddChar.Basic -import LeanAPAP.Prereqs.Convolution.Order -import LeanAPAP.Prereqs.FourierTransform.Compact +import LeanAPAP.Prereqs.Convolution.Discrete.Basic +import LeanAPAP.Prereqs.Expect.Complex +import LeanAPAP.Prereqs.FourierTransform.Discrete noncomputable section diff --git a/LeanAPAP/Prereqs/FourierTransform/Compact.lean b/LeanAPAP/Prereqs/FourierTransform/Compact.lean index b3caf848b1..1ba57ac97f 100644 --- a/LeanAPAP/Prereqs/FourierTransform/Compact.lean +++ b/LeanAPAP/Prereqs/FourierTransform/Compact.lean @@ -1,6 +1,7 @@ import LeanAPAP.Prereqs.Convolution.Compact -import LeanAPAP.Prereqs.FourierTransform.Discrete import LeanAPAP.Prereqs.Expect.Complex +import LeanAPAP.Prereqs.FourierTransform.Discrete +import LeanAPAP.Prereqs.Function.Indicator.Basic /-! # Discrete Fourier transform in the compact normalisation diff --git a/lake-manifest.json b/lake-manifest.json index 0a355a51dd..3cef812756 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "c8013cf7e8ac16ecaa8d30d18799360769ea5e8b", + "rev": "79ef7496100b18304654c1476691e872fa7c491a", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,