From 0e6c20df77ad46fe190fa78b419ed6a38a542593 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sun, 25 Aug 2024 20:12:56 +0000 Subject: [PATCH] Bump mathlib --- LeanAPAP.lean | 7 -- LeanAPAP/FiniteField/Basic.lean | 2 - LeanAPAP/Mathlib/Data/Finset/Density.lean | 11 ---- .../Mathlib/Data/Nat/Cast/Order/Basic.lean | 8 --- LeanAPAP/Mathlib/Data/Real/Sqrt.lean | 5 -- .../MeasureTheory/Function/EssSup.lean | 2 +- .../Mathlib/MeasureTheory/Measure/Count.lean | 17 ----- .../Mathlib/MeasureTheory/Measure/Dirac.lean | 11 ---- .../MeasureTheory/Measure/MeasureSpace.lean | 21 ------ LeanAPAP/Prereqs/AddChar/Basic.lean | 1 - LeanAPAP/Prereqs/AddChar/Defs.lean | 66 ------------------- .../Prereqs/AddChar/PontryaginDuality.lean | 1 + LeanAPAP/Prereqs/Bohr/Basic.lean | 1 - LeanAPAP/Prereqs/Energy.lean | 4 +- LeanAPAP/Prereqs/LpNorm/Compact.lean | 2 +- LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean | 2 +- LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean | 2 +- lake-manifest.json | 4 +- 18 files changed, 9 insertions(+), 158 deletions(-) delete mode 100644 LeanAPAP/Mathlib/Data/Finset/Density.lean delete mode 100644 LeanAPAP/Mathlib/Data/Nat/Cast/Order/Basic.lean delete mode 100644 LeanAPAP/Mathlib/Data/Real/Sqrt.lean delete mode 100644 LeanAPAP/Mathlib/MeasureTheory/Measure/Count.lean delete mode 100644 LeanAPAP/Mathlib/MeasureTheory/Measure/Dirac.lean delete mode 100644 LeanAPAP/Mathlib/MeasureTheory/Measure/MeasureSpace.lean delete mode 100644 LeanAPAP/Prereqs/AddChar/Defs.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index 5b232ded15..b34e17bff4 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -11,18 +11,12 @@ import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real import LeanAPAP.Mathlib.Data.ENNReal.Basic import LeanAPAP.Mathlib.Data.ENNReal.Operations import LeanAPAP.Mathlib.Data.ENNReal.Real -import LeanAPAP.Mathlib.Data.Finset.Density import LeanAPAP.Mathlib.Data.Fintype.Order import LeanAPAP.Mathlib.Data.NNReal.Basic -import LeanAPAP.Mathlib.Data.Nat.Cast.Order.Basic import LeanAPAP.Mathlib.Data.Rat.Cast.Order -import LeanAPAP.Mathlib.Data.Real.Sqrt import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic import LeanAPAP.Mathlib.MeasureTheory.MeasurableSpace.Defs -import LeanAPAP.Mathlib.MeasureTheory.Measure.Count -import LeanAPAP.Mathlib.MeasureTheory.Measure.Dirac -import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpace import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef import LeanAPAP.Mathlib.MeasureTheory.Measure.Typeclasses import LeanAPAP.Mathlib.Order.Filter.Basic @@ -32,7 +26,6 @@ import LeanAPAP.Physics.AlmostPeriodicity import LeanAPAP.Physics.DRC import LeanAPAP.Physics.Unbalancing import LeanAPAP.Prereqs.AddChar.Basic -import LeanAPAP.Prereqs.AddChar.Defs import LeanAPAP.Prereqs.AddChar.PontryaginDuality import LeanAPAP.Prereqs.Bohr.Basic import LeanAPAP.Prereqs.Bohr.Regular diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean index 5c7937a4c8..930e33995d 100644 --- a/LeanAPAP/FiniteField/Basic.lean +++ b/LeanAPAP/FiniteField/Basic.lean @@ -1,8 +1,6 @@ import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real -import LeanAPAP.Mathlib.Data.Finset.Density -import LeanAPAP.Mathlib.Data.Nat.Cast.Order.Basic import LeanAPAP.Mathlib.Data.Rat.Cast.Order import LeanAPAP.Prereqs.Convolution.ThreeAP import LeanAPAP.Prereqs.FourierTransform.Compact diff --git a/LeanAPAP/Mathlib/Data/Finset/Density.lean b/LeanAPAP/Mathlib/Data/Finset/Density.lean deleted file mode 100644 index 8c9cc4bb7b..0000000000 --- a/LeanAPAP/Mathlib/Data/Finset/Density.lean +++ /dev/null @@ -1,11 +0,0 @@ -import Mathlib.Data.Finset.Density - -open Function - -namespace Finset -variable {α β : Type*} [Fintype α] [Fintype β] [DecidableEq β] {f : α → β} - -lemma dens_image (hf : Bijective f) (s : Finset α) : (s.image f).dens = s.dens := by - simpa [map_eq_image, -dens_map_equiv] using dens_map_equiv (.ofBijective f hf) - -end Finset diff --git a/LeanAPAP/Mathlib/Data/Nat/Cast/Order/Basic.lean b/LeanAPAP/Mathlib/Data/Nat/Cast/Order/Basic.lean deleted file mode 100644 index 1761a7e432..0000000000 --- a/LeanAPAP/Mathlib/Data/Nat/Cast/Order/Basic.lean +++ /dev/null @@ -1,8 +0,0 @@ -import Mathlib.Data.Nat.Cast.Order.Basic - -namespace Nat - -@[gcongr] protected alias ⟨_, GCongr.cast_le_cast⟩ := Nat.cast_le -@[gcongr] protected alias ⟨_, GCongr.cast_lt_cast⟩ := Nat.cast_lt - -end Nat diff --git a/LeanAPAP/Mathlib/Data/Real/Sqrt.lean b/LeanAPAP/Mathlib/Data/Real/Sqrt.lean deleted file mode 100644 index abd845c07e..0000000000 --- a/LeanAPAP/Mathlib/Data/Real/Sqrt.lean +++ /dev/null @@ -1,5 +0,0 @@ -/-! -# TODO - -Replace `Real.sqrt_eq_iff_sq_eq` by `Real.sqrt_eq_iff_eq_sq` --/ diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean index 41aa553bf1..e191ff525b 100644 --- a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean +++ b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean @@ -1,5 +1,5 @@ import Mathlib.MeasureTheory.Function.EssSup -import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpace +import Mathlib.MeasureTheory.Measure.MeasureSpace import LeanAPAP.Mathlib.Order.LiminfLimsup open Filter MeasureTheory diff --git a/LeanAPAP/Mathlib/MeasureTheory/Measure/Count.lean b/LeanAPAP/Mathlib/MeasureTheory/Measure/Count.lean deleted file mode 100644 index ff46f593f5..0000000000 --- a/LeanAPAP/Mathlib/MeasureTheory/Measure/Count.lean +++ /dev/null @@ -1,17 +0,0 @@ -import Mathlib.MeasureTheory.Measure.Count -import LeanAPAP.Mathlib.MeasureTheory.Measure.Dirac -import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpace - -open Set - -namespace MeasureTheory.Measure -variable {α : Type*} {mα : MeasurableSpace α} - -@[simp] lemma count_univ [Fintype α] : count (univ : Set α) = Fintype.card α := by - rw [count_apply .univ] - refine (tsum_univ 1).trans ?_ - sorry - -@[simp] lemma count_ne_zero'' [Nonempty α] : (count : Measure α) ≠ 0 := by simp [count] - -end MeasureTheory.Measure diff --git a/LeanAPAP/Mathlib/MeasureTheory/Measure/Dirac.lean b/LeanAPAP/Mathlib/MeasureTheory/Measure/Dirac.lean deleted file mode 100644 index 794d757ece..0000000000 --- a/LeanAPAP/Mathlib/MeasureTheory/Measure/Dirac.lean +++ /dev/null @@ -1,11 +0,0 @@ -import Mathlib.MeasureTheory.Measure.Dirac - -open Set - -namespace MeasureTheory.Measure -variable {α : Type*} {mα : MeasurableSpace α} - -@[simp] lemma dirac_ne_zero (a : α) : dirac a ≠ 0 := - fun h ↦ by simpa [h] using dirac_apply_of_mem (mem_univ a) - -end MeasureTheory.Measure diff --git a/LeanAPAP/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/LeanAPAP/Mathlib/MeasureTheory/Measure/MeasureSpace.lean deleted file mode 100644 index 136e4cc91c..0000000000 --- a/LeanAPAP/Mathlib/MeasureTheory/Measure/MeasureSpace.lean +++ /dev/null @@ -1,21 +0,0 @@ -import Mathlib.MeasureTheory.Measure.MeasureSpace - -open scoped ENNReal - -namespace MeasureTheory.Measure -variable {ι α : Type*} {mα : MeasurableSpace α} {f : ι → Measure α} - -@[simp] lemma sum_eq_zero : sum f = 0 ↔ ∀ i, f i = 0 := by - simp (config := { contextual := true }) [Measure.ext_iff, forall_swap (α := ι)] - -variable {R : Type*} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] - [NoZeroSMulDivisors R ℝ≥0∞] {c : ℝ≥0∞} - --- TODO: Replace in mathlib -lemma ae_smul_measure_iff' {p : α → Prop} {c : R} (hc : c ≠ 0) {μ : Measure α} : - (∀ᵐ x ∂c • μ, p x) ↔ ∀ᵐ x ∂μ, p x := by simp [ae_iff, hc] - -@[simp] lemma ae_smul_measure_eq' (hc : c ≠ 0) (μ : Measure α) : ae (c • μ) = ae μ := by - ext; exact ae_smul_measure_iff hc - -end MeasureTheory.Measure diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean index f4d92cd669..bc3a2e599c 100644 --- a/LeanAPAP/Prereqs/AddChar/Basic.lean +++ b/LeanAPAP/Prereqs/AddChar/Basic.lean @@ -1,5 +1,4 @@ import LeanAPAP.Mathlib.Algebra.Group.AddChar -import LeanAPAP.Prereqs.AddChar.Defs import LeanAPAP.Prereqs.Expect.Basic import LeanAPAP.Prereqs.LpNorm.Discrete.Defs diff --git a/LeanAPAP/Prereqs/AddChar/Defs.lean b/LeanAPAP/Prereqs/AddChar/Defs.lean deleted file mode 100644 index 10ff5576fc..0000000000 --- a/LeanAPAP/Prereqs/AddChar/Defs.lean +++ /dev/null @@ -1,66 +0,0 @@ -import Mathlib.Algebra.DirectSum.Basic -import Mathlib.Algebra.Group.AddChar -import Mathlib.Analysis.RCLike.Basic - -open Finset hiding card -open Fintype (card) -open Function -open scoped ComplexConjugate DirectSum NNRat - -variable {G H R : Type*} - -namespace AddChar -section AddGroup -variable [AddGroup G] - -section NormedField -variable [NormedField R] - -@[simp] lemma coe_ne_zero (ψ : AddChar G R) : (ψ : G → R) ≠ 0 := - ne_iff.2 ⟨0, fun h ↦ by simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_eq_one ψ⟩ - -variable [Finite G] - -@[simp] lemma norm_apply (ψ : AddChar G R) (x : G) : ‖ψ x‖ = 1 := - (ψ.toMonoidHom.isOfFinOrder $ isOfFinOrder_of_finite _).norm_eq_one - -end NormedField - -section RCLike -variable [RCLike R] - -lemma inv_apply_eq_conj [Finite G] (ψ : AddChar G R) (x : G) : (ψ x)⁻¹ = conj (ψ x) := - RCLike.inv_eq_conj $ norm_apply _ _ - -end RCLike -end AddGroup - -section AddCommGroup -variable [AddCommGroup G] - -section RCLike -variable [RCLike R] {ψ₁ ψ₂ : AddChar G R} - -lemma map_neg_eq_conj [Finite G] (ψ : AddChar G R) (x : G) : ψ (-x) = conj (ψ x) := by - rw [map_neg_eq_inv, RCLike.inv_eq_conj $ norm_apply _ _] - -end RCLike - -end AddCommGroup - -section DirectSum -variable {ι : Type*} {π : ι → Type*} [DecidableEq ι] [∀ i, AddCommGroup (π i)] [CommMonoid R] - -/-- Direct sum of additive characters. -/ -protected def directSum (ψ : ∀ i, AddChar (π i) R) : AddChar (⨁ i, π i) R := - AddChar.toAddMonoidHomEquiv.symm - (DirectSum.toAddMonoid fun i ↦ toAddMonoidHomEquiv (ψ i) : (⨁ i, π i) →+ Additive R) - -lemma directSum_injective : - Injective (AddChar.directSum : (∀ i, AddChar (π i) R) → AddChar (⨁ i, π i) R) := by - refine AddChar.toAddMonoidHomEquiv.symm.injective.comp $ DirectSum.toAddMonoid_injective.comp ?_ - rintro ψ χ h - simpa [Function.funext_iff] using h - -end DirectSum -end AddChar diff --git a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean index bb06ec07e6..4a7f2b6b28 100644 --- a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean +++ b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean @@ -1,3 +1,4 @@ +import Mathlib.Algebra.DirectSum.AddChar import Mathlib.GroupTheory.FiniteAbelian import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar import LeanAPAP.Prereqs.AddChar.Basic diff --git a/LeanAPAP/Prereqs/Bohr/Basic.lean b/LeanAPAP/Prereqs/Bohr/Basic.lean index 0cd90c747f..ff2fbe4309 100644 --- a/LeanAPAP/Prereqs/Bohr/Basic.lean +++ b/LeanAPAP/Prereqs/Bohr/Basic.lean @@ -1,5 +1,4 @@ import Mathlib.Analysis.Complex.Basic -import LeanAPAP.Prereqs.AddChar.Defs open AddChar Complex Function open scoped NNReal diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean index d7cebdc08a..f8acf1446f 100644 --- a/LeanAPAP/Prereqs/Energy.lean +++ b/LeanAPAP/Prereqs/Energy.lean @@ -63,6 +63,6 @@ lemma nlpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) : Complex.coe_iterConv, Complex.ofReal_comp_indicate] lemma nl2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt s.card := by - rw [eq_comm, sqrt_eq_iff_sq_eq] - simpa using nlpNorm_dft_indicate_pow 1 s + rw [eq_comm, sqrt_eq_iff_eq_sq] + simpa [eq_comm] using nlpNorm_dft_indicate_pow 1 s all_goals positivity diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean index 2e8646cd4e..408274ca37 100644 --- a/LeanAPAP/Prereqs/LpNorm/Compact.lean +++ b/LeanAPAP/Prereqs/LpNorm/Compact.lean @@ -507,7 +507,7 @@ lemma nl2Norm_sq_indicate (s : Finset α) : ‖𝟭_[β] s‖ₙ_[2] ^ 2 = s.den simpa using nlpNorm_pow_indicate two_ne_zero s lemma nl2Norm_indicate (s : Finset α) : ‖𝟭_[β] s‖ₙ_[2] = Real.sqrt s.dens := by - rw [eq_comm, sqrt_eq_iff_sq_eq, nl2Norm_sq_indicate] <;> positivity + rw [eq_comm, sqrt_eq_iff_eq_sq, nl2Norm_sq_indicate] <;> positivity @[simp] lemma nl1Norm_indicate (s : Finset α) : ‖𝟭_[β] s‖ₙ_[1] = s.dens := by simpa using nlpNorm_pow_indicate one_ne_zero s diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean index f3d1937c12..fbb8b4b24d 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean @@ -98,7 +98,7 @@ lemma l2Norm_sq_indicate (s : Finset α) : ‖𝟭_[β] s‖_[2] ^ 2 = s.card := simpa using lpNorm_pow_indicate two_ne_zero s lemma l2Norm_indicate (s : Finset α) : ‖𝟭_[β] s‖_[2] = Real.sqrt s.card := by - rw [eq_comm, sqrt_eq_iff_sq_eq, l2Norm_sq_indicate] <;> positivity + rw [eq_comm, sqrt_eq_iff_eq_sq, l2Norm_sq_indicate] <;> positivity @[simp] lemma l1Norm_indicate (s : Finset α) : ‖𝟭_[β] s‖_[1] = s.card := by simpa using lpNorm_pow_indicate one_ne_zero s diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean index cb36566326..8033bb2053 100644 --- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean +++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean @@ -127,7 +127,7 @@ private lemma step_four {k : Fin n → ℕ} : · norm_num split_ifs with h · rw [h.neg_one_pow, one_add_one_eq_two] - rw [← Nat.odd_iff_not_even] at h + rw [Nat.not_even_iff_odd] at h simp [h.neg_one_pow] -- double_multinomial diff --git a/lake-manifest.json b/lake-manifest.json index ddc523df08..9509d9de82 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9339d48cc3b7431b6353af47f303691e9d4da229", + "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7ed205ef984ad7571fa0d6f21e444be1731d200b", + "rev": "9b07fb6d08b58de5b55813b29f5ac9aa6fa0b1ad", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,