From 0db79d9f30bd2fbe5cd53faa35504bc698e9d344 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 26 Nov 2024 13:58:24 +0000 Subject: [PATCH] Bump mathlib --- LeanAPAP.lean | 5 +- .../Order/GroupWithZero/Unbundled.lean | 10 --- .../Function/LpSeminorm/Basic.lean | 73 ------------------- LeanAPAP/Mathlib/Probability/UniformOn.lean | 8 -- LeanAPAP/Physics/AlmostPeriodicity.lean | 1 - LeanAPAP/Prereqs/Chang.lean | 1 - LeanAPAP/Prereqs/Convolution/Order.lean | 2 +- .../DummyPositivity.lean} | 0 LeanAPAP/Prereqs/NNLpNorm.lean | 8 +- lake-manifest.json | 4 +- 10 files changed, 6 insertions(+), 106 deletions(-) delete mode 100644 LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean delete mode 100644 LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean delete mode 100644 LeanAPAP/Mathlib/Probability/UniformOn.lean rename LeanAPAP/{Mathlib/Tactic/Positivity.lean => Prereqs/DummyPositivity.lean} (100%) diff --git a/LeanAPAP.lean b/LeanAPAP.lean index 72421693bd..61e8600b03 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -1,10 +1,6 @@ import LeanAPAP.Extras.BSG import LeanAPAP.FiniteField import LeanAPAP.Integer -import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled -import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic -import LeanAPAP.Mathlib.Probability.UniformOn -import LeanAPAP.Mathlib.Tactic.Positivity import LeanAPAP.Physics.AlmostPeriodicity import LeanAPAP.Physics.DRC import LeanAPAP.Physics.Unbalancing @@ -18,6 +14,7 @@ import LeanAPAP.Prereqs.Convolution.Discrete.Defs import LeanAPAP.Prereqs.Convolution.Norm import LeanAPAP.Prereqs.Convolution.Order import LeanAPAP.Prereqs.Convolution.ThreeAP +import LeanAPAP.Prereqs.DummyPositivity import LeanAPAP.Prereqs.Energy import LeanAPAP.Prereqs.FourierTransform.Compact import LeanAPAP.Prereqs.FourierTransform.Convolution diff --git a/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean b/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean deleted file mode 100644 index bc8de6bd9b..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean +++ /dev/null @@ -1,10 +0,0 @@ -import Mathlib.Algebra.Order.GroupWithZero.Unbundled - -@[bound] alias ⟨_, Bound.one_le_inv₀⟩ := one_le_inv₀ - -attribute [bound] mul_le_one₀ - -@[bound] -protected lemma Bound.one_lt_mul {M₀ : Type*} [MonoidWithZero M₀] [Preorder M₀] [ZeroLEOneClass M₀] - [PosMulMono M₀] [MulPosMono M₀] {a b : M₀} : 1 ≤ a ∧ 1 < b ∨ 1 < a ∧ 1 ≤ b → 1 < a * b := by - rintro (⟨ha, hb⟩ | ⟨ha, hb⟩); exacts [one_lt_mul ha hb, one_lt_mul_of_lt_of_le ha hb] diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean deleted file mode 100644 index 384c57bd63..0000000000 --- a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean +++ /dev/null @@ -1,73 +0,0 @@ -import Mathlib.Data.Fintype.Order -import Mathlib.MeasureTheory.Function.LpSeminorm.Basic - -noncomputable section - -open TopologicalSpace MeasureTheory Filter -open scoped NNReal ENNReal Topology ComplexConjugate - -variable {α E F G : Type*} {m m0 : MeasurableSpace α} {p : ℝ≥0∞} {q : ℝ} {μ ν : Measure α} - [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F} - -namespace MeasureTheory - -lemma eLpNormEssSup_lt_top_iff_isBoundedUnder : - eLpNormEssSup f μ < ⊤ ↔ IsBoundedUnder (· ≤ ·) (ae μ) fun x ↦ ‖f x‖₊ where - mp h := ⟨(eLpNormEssSup f μ).toNNReal, by - simp_rw [← ENNReal.coe_le_coe, ENNReal.coe_toNNReal h.ne]; exact ae_le_eLpNormEssSup⟩ - mpr := by rintro ⟨C, hC⟩; exact eLpNormEssSup_lt_top_of_ae_nnnorm_bound (C := C) hC - -lemma eLpNorm_lt_top_of_finite [Finite α] [IsFiniteMeasure μ] : eLpNorm f p μ < ∞ := by - obtain rfl | hp₀ := eq_or_ne p 0 - · simp - obtain rfl | hp := eq_or_ne p ∞ - · simp only [eLpNorm_exponent_top, eLpNormEssSup_lt_top_iff_isBoundedUnder] - exact .le_of_finite - rw [eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top hp₀ hp] - refine IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal μ ?_ - simp_rw [← ENNReal.coe_rpow_of_nonneg _ ENNReal.toReal_nonneg] - norm_cast - exact Finite.exists_le _ - -@[simp] lemma Memℒp.of_discrete [DiscreteMeasurableSpace α] [Finite α] [IsFiniteMeasure μ] : - Memℒp f p μ := - let ⟨C, hC⟩ := Finite.exists_le (‖f ·‖₊); .of_bound .of_finite C <| .of_forall hC - -@[simp] lemma eLpNorm_of_isEmpty [IsEmpty α] (f : α → E) (p : ℝ≥0∞) : eLpNorm f p μ = 0 := by - simp [Subsingleton.elim f 0] - --- TODO: Make `p` and `μ` explicit in `eLpNorm_const_smul`, `eLpNorm_neg` - -@[simp] lemma eLpNorm_neg' (f : α → F) (p : ℝ≥0∞) (μ : Measure α) : - eLpNorm (fun x ↦ -f x) p μ = eLpNorm f p μ := eLpNorm_neg - -lemma eLpNorm_sub_comm (f g : α → E) (p : ℝ≥0∞) (μ : Measure α) : - eLpNorm (f - g) p μ = eLpNorm (g - f) p μ := by simp [← eLpNorm_neg (f := f - g)] - -lemma eLpNorm_nsmul [NormedSpace ℝ F] (n : ℕ) (f : α → F) : - eLpNorm (n • f) p μ = n * eLpNorm f p μ := by - simpa [Nat.cast_smul_eq_nsmul] using eLpNorm_const_smul (n : ℝ) f - --- TODO: Replace `eLpNorm_smul_measure_of_ne_zero` -lemma eLpNorm_smul_measure_of_ne_zero' {c : ℝ≥0∞} (hc : c ≠ 0) (f : α → F) (p : ℝ≥0∞) - (μ : Measure α) : eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ * eLpNorm f p μ := by - simpa using eLpNorm_smul_measure_of_ne_zero hc - -lemma eLpNorm_smul_measure_of_ne_zero'' {c : ℝ≥0} (hc : c ≠ 0) (f : α → F) (p : ℝ≥0∞) - (μ : Measure α) : eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ := - (eLpNorm_smul_measure_of_ne_zero (ENNReal.coe_ne_zero.2 hc)).trans (by simp; norm_cast) - -lemma eLpNorm_smul_measure_of_ne_top' (hp : p ≠ ∞) (c : ℝ≥0∞) (f : α → F) : - eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ * eLpNorm f p μ := by - simpa using eLpNorm_smul_measure_of_ne_top hp _ - -lemma eLpNorm_smul_measure_of_ne_top'' (hp : p ≠ ∞) (c : ℝ≥0) (f : α → F) : - eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ := by - have : 0 ≤ p.toReal⁻¹ := by positivity - refine (eLpNorm_smul_measure_of_ne_top' hp _ _).trans ?_ - simp [ENNReal.smul_def, ENNReal.coe_rpow_of_nonneg, this] - -@[simp] lemma eLpNorm_conj {K : Type*} [RCLike K] (f : α → K) (p : ℝ≥0∞) (μ : Measure α) : - eLpNorm (conj f) p μ = eLpNorm f p μ := by simp [← eLpNorm_norm] - -end MeasureTheory diff --git a/LeanAPAP/Mathlib/Probability/UniformOn.lean b/LeanAPAP/Mathlib/Probability/UniformOn.lean deleted file mode 100644 index 24ab9172d4..0000000000 --- a/LeanAPAP/Mathlib/Probability/UniformOn.lean +++ /dev/null @@ -1,8 +0,0 @@ -import Mathlib.Probability.UniformOn - -namespace ProbabilityTheory -variable {Ω : Type*} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} - -@[simp] lemma uniformOn_eq_zero : uniformOn s = 0 ↔ s.Infinite ∨ s = ∅ := by simp [uniformOn] - -end ProbabilityTheory diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index 98a41e1fcd..f7db7df333 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -2,7 +2,6 @@ import Mathlib.Algebra.Order.Chebyshev import Mathlib.Combinatorics.Additive.DoublingConst import Mathlib.Data.Complex.ExponentialBounds import Mathlib.Tactic.Bound -import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled import LeanAPAP.Prereqs.Convolution.Discrete.Basic import LeanAPAP.Prereqs.Convolution.Norm import LeanAPAP.Prereqs.Inner.Hoelder.Discrete diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean index a0226e897e..737425e76a 100644 --- a/LeanAPAP/Prereqs/Chang.lean +++ b/LeanAPAP/Prereqs/Chang.lean @@ -1,7 +1,6 @@ import Mathlib.Algebra.Order.Chebyshev import Mathlib.Analysis.MeanInequalities import Mathlib.Tactic.Bound -import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled import LeanAPAP.Prereqs.Energy import LeanAPAP.Prereqs.LargeSpec import LeanAPAP.Prereqs.Rudin diff --git a/LeanAPAP/Prereqs/Convolution/Order.lean b/LeanAPAP/Prereqs/Convolution/Order.lean index 828a9c3f20..5ffe8f8cce 100644 --- a/LeanAPAP/Prereqs/Convolution/Order.lean +++ b/LeanAPAP/Prereqs/Convolution/Order.lean @@ -1,5 +1,5 @@ import Mathlib.Algebra.Order.Star.Conjneg -import LeanAPAP.Mathlib.Tactic.Positivity +import LeanAPAP.Prereqs.DummyPositivity import LeanAPAP.Prereqs.Convolution.Discrete.Defs open Finset Function Real diff --git a/LeanAPAP/Mathlib/Tactic/Positivity.lean b/LeanAPAP/Prereqs/DummyPositivity.lean similarity index 100% rename from LeanAPAP/Mathlib/Tactic/Positivity.lean rename to LeanAPAP/Prereqs/DummyPositivity.lean diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean index 1f01d80597..4646009382 100644 --- a/LeanAPAP/Prereqs/NNLpNorm.lean +++ b/LeanAPAP/Prereqs/NNLpNorm.lean @@ -1,9 +1,5 @@ -import Mathlib.Algebra.BigOperators.Expect -import Mathlib.Algebra.Order.Module.Rat -import Mathlib.Analysis.Normed.Group.Constructions import Mathlib.MeasureTheory.Integral.Bochner import Mathlib.Tactic.Positivity.Finset -import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic open Filter open scoped BigOperators ComplexConjugate ENNReal NNReal @@ -184,11 +180,11 @@ lemma nnLpNorm_mono_real {g : α → ℝ} (hg : Memℒp g p μ) (h : ∀ x, ‖f lemma nnLpNorm_smul_measure_of_ne_zero {f : α → E} {c : ℝ≥0} (hc : c ≠ 0) : nnLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • nnLpNorm f p μ := by - simp [nnLpNorm, eLpNorm_smul_measure_of_ne_zero'' hc f p μ] + simp [nnLpNorm, eLpNorm_smul_measure_of_ne_zero' hc f p μ] lemma nnLpNorm_smul_measure_of_ne_top (hp : p ≠ ∞) {f : α → E} (c : ℝ≥0) : nnLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • nnLpNorm f p μ := by - simp [nnLpNorm, eLpNorm_smul_measure_of_ne_top'' hp] + simp [nnLpNorm, eLpNorm_smul_measure_of_ne_top' hp] @[simp] lemma nnLpNorm_conj {K : Type*} [RCLike K] (f : α → K) (p : ℝ≥0∞) (μ : Measure α) : nnLpNorm (conj f) p μ = nnLpNorm f p μ := by simp [← nnLpNorm_norm] diff --git a/lake-manifest.json b/lake-manifest.json index 74df2e8009..ea06098cf0 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "485efbc439ee0ebdeae8afb0acd24a5e82e2f771", + "rev": "7488499a8aad6ffada87ab6db73673d88dc04c97", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "fb23240e8b4409f2f23bcd07aa73c7451f216413", + "rev": "5ad34c033417c6e6efd3fcd9062fa1764d240209", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,