From 0b74d91266ebdfff080578f30e54304d7a0e2652 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 14 Jan 2025 17:56:17 +0000 Subject: [PATCH] Bump mathlib --- LeanAPAP.lean | 2 -- LeanAPAP/FiniteField.lean | 6 ++--- .../MeasureTheory/Function/LpSpace.lean | 8 ------ .../MeasureTheory/Integral/Bochner.lean | 9 ------- LeanAPAP/Physics/AlmostPeriodicity.lean | 2 +- LeanAPAP/Physics/DRC.lean | 4 +-- LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean | 9 ++++--- LeanAPAP/Prereqs/NewMarcinkiewiczZygmund.lean | 1 - lake-manifest.json | 26 +++++++++---------- lean-toolchain | 2 +- 10 files changed, 25 insertions(+), 44 deletions(-) delete mode 100644 LeanAPAP/Mathlib/MeasureTheory/Function/LpSpace.lean delete mode 100644 LeanAPAP/Mathlib/MeasureTheory/Integral/Bochner.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index 9881d40d2a..69c32b9a5c 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -1,8 +1,6 @@ import LeanAPAP.Extras.BSG import LeanAPAP.FiniteField import LeanAPAP.Integer -import LeanAPAP.Mathlib.MeasureTheory.Function.LpSpace -import LeanAPAP.Mathlib.MeasureTheory.Integral.Bochner import LeanAPAP.Physics.AlmostPeriodicity import LeanAPAP.Physics.DRC import LeanAPAP.Physics.Unbalancing diff --git a/LeanAPAP/FiniteField.lean b/LeanAPAP/FiniteField.lean index 2fd03ee82c..8d6bdc4849 100644 --- a/LeanAPAP/FiniteField.lean +++ b/LeanAPAP/FiniteField.lean @@ -461,8 +461,8 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr (B.dens < (65 / 64 : ℝ) ^ i * α → 2⁻¹ ≤ card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) := by induction' i with i ih hi - · exact ⟨G, inferInstance, inferInstance, inferInstance, inferInstance, A, by simp, hA, - by simp, by simp [α, nnratCast_dens, Fintype.card_subtype, subset_iff]⟩ + · exact ⟨G, inferInstance, inferInstance, inferInstance, inferInstance, A, by simp [n], hA, + by simp [α], by simp [α, nnratCast_dens, Fintype.card_subtype, subset_iff]⟩ obtain ⟨V, _, _, _, _, B, hV, hB, hαβ, hBV⟩ := ih obtain hB' | hB' := le_or_lt 2⁻¹ (card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) · exact ⟨V, inferInstance, inferInstance, inferInstance, inferInstance, B, @@ -486,7 +486,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr _ ≤ ‖(𝟭_[ℝ] B ∗ μ (V' : Set V).toFinset) x‖ := hx _ = B'.dens := ?_ rw [mu, conv_smul, Pi.smul_apply, indicate_conv_indicate_eq_card_vadd_inter_neg, - norm_of_nonneg (by positivity), nnratCast_dens, card_preimage, smul_eq_mul, inv_mul_eq_div] + Real.norm_of_nonneg (by positivity), nnratCast_dens, card_preimage, smul_eq_mul, inv_mul_eq_div] congr 2 · congr 1 with x simp diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSpace.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSpace.lean deleted file mode 100644 index 0a3127129c..0000000000 --- a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSpace.lean +++ /dev/null @@ -1,8 +0,0 @@ -import Mathlib.MeasureTheory.Function.LpSpace - -namespace MeasureTheory.Memℒp -variable {α E : Type*} {m0 : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] - [NormedAddCommGroup E] {p q : ENNReal} {f : α → E} - -lemma mono_exponent (hpq : p ≤ q) (hfq : Memℒp f q μ) : Memℒp f p μ := - hfq.memℒp_of_exponent_le_of_measure_support_ne_top (by simp) (measure_ne_top _ .univ) hpq diff --git a/LeanAPAP/Mathlib/MeasureTheory/Integral/Bochner.lean b/LeanAPAP/Mathlib/MeasureTheory/Integral/Bochner.lean deleted file mode 100644 index e65b38a511..0000000000 --- a/LeanAPAP/Mathlib/MeasureTheory/Integral/Bochner.lean +++ /dev/null @@ -1,9 +0,0 @@ -import Mathlib.MeasureTheory.Integral.Bochner - -namespace MeasureTheory -variable {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} - -lemma abs_integral_le_integral_abs : |∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ := - norm_integral_le_integral_norm f - -end MeasureTheory diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index f7db7df333..e37de5b215 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -138,7 +138,7 @@ lemma lemma28_part_one (hm : 1 ≤ m) (x : G) : simp only [boole_mul, indicate_apply] rw [← sum_filter, filter_mem_eq_inter, univ_inter, sub_self, smul_zero] congr with a : 1 - simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin] + simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin, f'] lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) : (∑ x ∈ L + S.piDiag (Fin k), ∑ l ∈ L, ∑ s ∈ S.piDiag (Fin k), ite (l + s = x) (1 : ℝ) 0) ^ 2 diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index 1b45359474..9f1fc3a60d 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/LeanAPAP/Physics/DRC.lean @@ -128,7 +128,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) $ hg s).le, this.trans $ mul_le_of_le_one_right ?_ $ div_le_one_of_le₀ ?_ ?_, this.trans $ mul_le_of_le_one_left ?_ $ div_le_one_of_le₀ ?_ ?_⟩ · simp_rw [A₁, A₂, g, ← card_smul_mu, smul_dconv, dconv_smul, ← Nat.cast_smul_eq_nsmul ℝ, - wInner_smul_left, smul_eq_mul, star_trivial, mul_assoc] + wInner_smul_left, smul_eq_mul, star_trivial, mul_assoc, A₁, A₂] any_goals positivity all_goals exact Nat.cast_le.2 $ card_mono inter_subset_left rw [← sum_mul, lemma_0, nsmul_eq_mul, Nat.cast_mul, ← sum_mul, mul_right_comm, ← hgB, @@ -156,7 +156,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ := sum_lt_sum_of_nonempty ⟨s, mem_filter.2 ⟨mem_univ _, hs.symm⟩⟩ ?_ _ ≤ ∑ s, M * sqrt (g s) := sum_le_univ_sum_of_nonneg fun s ↦ by positivity _ = M * (∑ s, sqrt #(A₁ s) * sqrt #(A₂ s)) - := by simp_rw [mul_sum, sqrt_mul $ Nat.cast_nonneg _] + := by simp_rw [mul_sum, g, sqrt_mul $ Nat.cast_nonneg _] _ ≤ M * (sqrt (∑ s, #(A₁ s)) * sqrt (∑ s, #(A₂ s))) := by gcongr; exact sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity _ = _ := ?_ diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean index 7ed8dd2b6a..1c1de1996f 100644 --- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean +++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean @@ -27,7 +27,7 @@ private lemma step_one (hA : A.Nonempty) (f : ι → ℝ) (a : Fin n → ι) calc |∑ i, f (a i)| ^ (m + 1) = |∑ i, (f (a i) - (∑ b ∈ B, f (b i)) / #B)| ^ (m + 1) := by - simp only [hf, sub_zero, zero_div] + simp only [B, hf, sub_zero, zero_div] _ = |(∑ b ∈ B, ∑ i, (f (a i) - f (b i))) / #B| ^ (m + 1) := by simp only [sum_sub_distrib] rw [sum_const, sub_div, sum_comm, sum_div, nsmul_eq_mul, card_piFinset, prod_const, @@ -72,18 +72,18 @@ private lemma step_two_aux (A : Finset ι) (f : ι → ℝ) (ε : Fin n → ℝ) intro xy exact (fun i ↦ if ε i = 1 then xy.1 i else xy.2 i, fun i ↦ if ε i = 1 then xy.2 i else xy.1 i) have h₁ : ∀ a ∈ (A ^^ n) ×ˢ (A ^^ n), swapper a ∈ (A ^^ n) ×ˢ (A ^^ n) := by - simp only [mem_product, and_imp, mem_piFinset, ← forall_and] + simp only [mem_product, and_imp, mem_piFinset, ← forall_and, swapper] intro a h i split_ifs · exact h i · exact (h i).symm have h₂ : ∀ a ∈ (A ^^ n) ×ˢ (A ^^ n), swapper (swapper a) = a := fun a _ ↦ by - ext <;> simp only <;> split_ifs <;> rfl + ext <;> simp only [swapper] <;> split_ifs <;> rfl refine sum_nbij' swapper swapper h₁ h₁ h₂ h₂ ?_ · rintro ⟨a, b⟩ _ congr with i : 1 - simp only [Pi.mul_apply, Pi.sub_apply, Function.comp_apply] simp only [mem_piFinset, mem_insert, mem_singleton] at hε + simp only [Pi.mul_apply, Pi.sub_apply, Function.comp_apply, swapper] split_ifs with h · simp [h] rw [(hε i).resolve_right h] @@ -171,6 +171,7 @@ private lemma end_step {f : ι → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) : add_assoc, Nat.sub_add_cancel hm, pow_add, ← mul_pow, ← mul_pow, card_piFinset, prod_const, Finset.card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀] norm_num + dsimp [B] positivity namespace Real diff --git a/LeanAPAP/Prereqs/NewMarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/NewMarcinkiewiczZygmund.lean index e9c36ab8f5..1e90914b72 100644 --- a/LeanAPAP/Prereqs/NewMarcinkiewiczZygmund.lean +++ b/LeanAPAP/Prereqs/NewMarcinkiewiczZygmund.lean @@ -5,7 +5,6 @@ Authors: Yaël Dillies, Bhavik Mehta -/ import Mathlib.Data.Nat.Choose.Multinomial import Mathlib.Probability.IdentDistrib -import LeanAPAP.Mathlib.MeasureTheory.Integral.Bochner /-! # The Marcinkiewicz-Zygmund inequality diff --git a/lake-manifest.json b/lake-manifest.json index c03bcbc0fb..65cc3a4de5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,20 +5,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608", + "rev": "1b272a8b24271676a3200364b9168fe3d4ada86e", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5", + "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -35,30 +35,30 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9a0b533c2fbd6195df067630be18e11e4349051c", + "rev": "f72319c9686788305a8ab059f3c4d8c724785c83", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2b000e02d50394af68cfb4770a291113d94801b5", + "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.48", + "inputRev": "v0.0.50", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2689851f387bb2cef351e6825fe94a56a304ca13", + "rev": "79402ad9ab4be9a2286701a9880697e2351e4955", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", @@ -75,10 +75,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", + "rev": "c104265c34eb8181af14e8dbc14c2f034292cb02", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -91,5 +91,5 @@ "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}], - "name": "LeanCamCombi", + "name": "LeanAPAP", "lakeDir": ".lake"} diff --git a/lean-toolchain b/lean-toolchain index d0eb99ff68..2ffc30ceba 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0 +leanprover/lean4:v4.16.0-rc2 \ No newline at end of file