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..64c4fd316f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,62 +1,72 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/batteries", + [{"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "485efbc439ee0ebdeae8afb0acd24a5e82e2f771", - "name": "batteries", + "scope": "", + "rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c", + "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", - "name": "Qq", + "scope": "", + "rev": "90f062feea36adad53b81925aa9dc3e09c268262", + "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, + "inputRev": null, + "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + {"url": "https://github.com/mhuisi/lean4-cli", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "de91b59101763419997026c35a41432ac8691f15", - "name": "aesop", + "scope": "", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", + {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "1383e72b40dd62a566896a6e348ffe868801b172", - "name": "proofwidgets", + "scope": "", + "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014", + "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.46", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/dupuisf/BibtexQuery", "type": "git", "subDir": null, - "scope": "leanprover", - "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", - "name": "Cli", + "scope": "", + "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005", + "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "119b022b3ea88ec810a677888528e50f8144a26e", - "name": "importGraph", + "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", + "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, @@ -71,65 +81,55 @@ "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/plausible", + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", - "name": "plausible", + "rev": "119b022b3ea88ec810a677888528e50f8144a26e", + "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "fb23240e8b4409f2f23bcd07aa73c7451f216413", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/acmepjz/md4lean", + {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "scope": "", - "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005", - "name": "MD4Lean", + "scope": "leanprover-community", + "rev": "1383e72b40dd62a566896a6e348ffe868801b172", + "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v0.0.46", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "scope": "", - "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014", - "name": "UnicodeBasic", + "scope": "leanprover-community", + "rev": "de91b59101763419997026c35a41432ac8691f15", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "master", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "scope": "", - "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", - "name": "BibtexQuery", + "scope": "leanprover-community", + "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", + "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/doc-gen4", + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "scope": "", - "rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c", - "name": "«doc-gen4»", + "scope": "leanprover-community", + "rev": "dfbe9387054e2972449de7bf346059d3609529fa", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}], + "inherited": true, + "configFile": "lakefile.toml"}], "name": "LeanAPAP", "lakeDir": ".lake"} diff --git a/lean-toolchain b/lean-toolchain index 57a4710c03..6d9e70f733 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc2 +leanprover/lean4:v4.14.0-rc3