From c3c8f06ffa3ad5aa898caf6817d3bb976b20f3a8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sun, 2 Feb 2025 11:37:24 +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 | 14 ++++---- LeanAPAP/Physics/Unbalancing.lean | 30 ++++++++-------- LeanAPAP/Prereqs/Chang.lean | 24 ++++++------- LeanAPAP/Prereqs/Energy.lean | 2 +- LeanAPAP/Prereqs/Function/Indicator/Defs.lean | 4 +-- LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean | 9 ++--- LeanAPAP/Prereqs/NNLpNorm.lean | 8 ++--- LeanAPAP/Prereqs/NewMarcinkiewiczZygmund.lean | 1 - docbuild/lake-manifest.json | 36 +++++++++---------- docbuild/lakefile.toml | 2 +- docbuild/lean-toolchain | 2 +- lake-manifest.json | 26 +++++++------- lean-toolchain | 2 +- 18 files changed, 84 insertions(+), 103 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..68019b0d10 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 _ = _ := ?_ @@ -172,7 +172,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p) (hp₂ : 2 ≤ p) (hpε : ε⁻¹ * log (2 / δ) ≤ p) (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty) (hf : ∃ x, x ∈ B₁ - B₂ ∧ x ∈ A - A ∧ x ∉ s p ε B₁ B₂ A) : - ∃ A₁, A₁ ⊆ B₁ ∧ ∃ A₂, A₂ ⊆ B₂ ∧ 1 - δ ≤ ∑ x in s p ε B₁ B₂ A, (μ A₁ ○ μ A₂) x ∧ + ∃ A₁, A₁ ⊆ B₁ ∧ ∃ A₂, A₂ ⊆ B₂ ∧ 1 - δ ≤ ∑ x ∈ s p ε B₁ B₂ A, (μ A₁ ○ μ A₂) x ∧ (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) ≤ #A₁ / #B₁ ∧ (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) ≤ @@ -196,7 +196,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 clear hcard₁ hcard₂ aux rw [sub_le_comm] calc - _ = ∑ x in (s p ε B₁ B₂ A)ᶜ, (μ A₁ ○ μ A₂) x := ?_ + _ = ∑ x ∈ (s p ε B₁ B₂ A)ᶜ, (μ A₁ ○ μ A₂) x := ?_ _ = ⟪μ_[ℝ] A₁ ○ μ A₂, (↑) ∘ 𝟭_[ℝ≥0] ((s (↑p) ε B₁ B₂ A)ᶜ)⟫_[ℝ] := by simp [wInner_one_eq_sum, -mem_compl, -mem_s, apply_ite NNReal.toReal, indicate_apply] _ ≤ _ := (le_div_iff₀ $ dLpNorm_conv_pos hp₀.ne' hB hA).2 h @@ -207,8 +207,8 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 simp only [apply_ite NNReal.toReal, indicate_apply, NNReal.coe_one, NNReal.coe_zero, mul_boole, Fintype.sum_ite_mem, mul_div_right_comm] calc - ∑ x in (s p ε B₁ B₂ A)ᶜ, (μ B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p ≤ - ∑ x in (s p ε B₁ B₂ A)ᶜ, + ∑ x ∈ (s p ε B₁ B₂ A)ᶜ, (μ B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p ≤ + ∑ x ∈ (s p ε B₁ B₂ A)ᶜ, (μ B₁ ○ μ B₂) x * ((1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂]) ^ p := by gcongr with x hx · exact Pi.le_def.1 (dconv_nonneg (R := ℝ) mu_nonneg mu_nonneg) x @@ -240,7 +240,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 /-- Special case of `sifting` when `B₁ = B₂ = univ`. -/ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p) (hp₂ : 2 ≤ p) (hpε : ε⁻¹ * log (2 / δ) ≤ p) (hA : A.Nonempty) : - ∃ A₁ A₂, 1 - δ ≤ ∑ x in s p ε univ univ A, (μ A₁ ○ μ A₂) x ∧ + ∃ A₁ A₂, 1 - δ ≤ ∑ x ∈ s p ε univ univ A, (μ A₁ ○ μ A₂) x ∧ (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤ A₁.dens ∧ (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤ A₂.dens := by by_cases hf : ∃ x, x ∈ A - A ∧ (𝟭 A ○ 𝟭 A) x ≤ (1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ univ] diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index 9999b40a39..58265719b5 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/LeanAPAP/Physics/Unbalancing.lean @@ -103,7 +103,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 set P : Finset _ := {i | 0 ≤ f i} set T : Finset _ := {i | 3 / 4 * ε ≤ f i} have hTP : T ⊆ P := monotone_filter_right _ fun i ↦ le_trans $ by positivity - have : 2⁻¹ * ε ^ p ≤ ∑ i in P, ↑(ν i) * (f ^ p) i := by + have : 2⁻¹ * ε ^ p ≤ ∑ i ∈ P, ↑(ν i) * (f ^ p) i := by rw [inv_mul_le_iff₀ (zero_lt_two' ℝ), sum_filter] convert this using 3 rw [Pi.posPart_apply, posPart_eq_ite] @@ -112,10 +112,10 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 norm_cast rw [Nat.succ_le_iff] positivity - have : ∑ i in P \ T, ↑(ν i) * (f ^ p) i ≤ 4⁻¹ * ε ^ p := by + have : ∑ i ∈ P \ T, ↑(ν i) * (f ^ p) i ≤ 4⁻¹ * ε ^ p := by calc - _ ≤ ∑ i in P \ T, ↑(ν i) * (3 / 4 * ε) ^ p := sum_le_sum fun i hi ↦ ?_ - _ = (3 / 4) ^ p * ε ^ p * ∑ i in P \ T, (ν i : ℝ) := by rw [← sum_mul, mul_comm, mul_pow] + _ ≤ ∑ i ∈ P \ T, ↑(ν i) * (3 / 4 * ε) ^ p := sum_le_sum fun i hi ↦ ?_ + _ = (3 / 4) ^ p * ε ^ p * ∑ i ∈ P \ T, (ν i : ℝ) := by rw [← sum_mul, mul_comm, mul_pow] _ ≤ 4⁻¹ * ε ^ p * ∑ i, (ν i : ℝ) := ?_ _ = 4⁻¹ * ε ^ p := by norm_cast; simp [hν₁] · simp only [mem_sdiff, mem_filter, mem_univ, true_and, not_le, P, T] at hi @@ -137,19 +137,19 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 simp [wLpNorm_one, ENNReal.mul_ne_top, *] _ = 3 := by norm_num replace hp' := zero_lt_one.trans_le hp' - have : 4⁻¹ * ε ^ p ≤ sqrt (∑ i in T, ν i) * 3 ^ p := by + have : 4⁻¹ * ε ^ p ≤ sqrt (∑ i ∈ T, ν i) * 3 ^ p := by calc 4⁻¹ * ε ^ p = 2⁻¹ * ε ^ p - 4⁻¹ * ε ^ p := by rw [← sub_mul]; norm_num _ ≤ _ := (sub_le_sub ‹_› ‹_›) - _ = ∑ i in T, ν i * (f ^ p) i := by rw [sum_sdiff_eq_sub hTP, sub_sub_cancel] - _ ≤ ∑ i in T, ν i * |(f ^ p) i| := + _ = ∑ i ∈ T, ν i * (f ^ p) i := by rw [sum_sdiff_eq_sub hTP, sub_sub_cancel] + _ ≤ ∑ i ∈ T, ν i * |(f ^ p) i| := (sum_le_sum fun i _ ↦ mul_le_mul_of_nonneg_left (le_abs_self _) ?_) - _ = ∑ i in T, sqrt (ν i) * sqrt (ν i * |(f ^ (2 * p)) i|) := by simp [← mul_assoc, pow_mul'] - _ ≤ sqrt (∑ i in T, ν i) * sqrt (∑ i in T, ν i * |(f ^ (2 * p)) i|) := + _ = ∑ i ∈ T, sqrt (ν i) * sqrt (ν i * |(f ^ (2 * p)) i|) := by simp [← mul_assoc, pow_mul'] + _ ≤ sqrt (∑ i ∈ T, ν i) * sqrt (∑ i ∈ T, ν i * |(f ^ (2 * p)) i|) := (sum_sqrt_mul_sqrt_le _ (fun i ↦ ?_) fun i ↦ ?_) - _ ≤ sqrt (∑ i in T, ν i) * sqrt (∑ i, ν i * |(f ^ (2 * p)) i|) := by + _ ≤ sqrt (∑ i ∈ T, ν i) * sqrt (∑ i, ν i * |(f ^ (2 * p)) i|) := by gcongr; exact T.subset_univ - _ = sqrt (∑ i in T, ν i) * ‖f‖_[2 * ↑p, ν] ^ p := ?_ + _ = sqrt (∑ i ∈ T, ν i) * ‖f‖_[2 * ↑p, ν] ^ p := ?_ _ ≤ _ := by gcongr; exact mod_cast hf₁ any_goals positivity rw [wLpNorm_eq_sum_nnnorm (mod_cast hp'.ne') (by simp [ENNReal.mul_ne_top])] @@ -159,7 +159,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 simp [mul_comm, this, Real.sqrt_eq_rpow] set p' := 24 / ε * log (3 / ε) * p have hp' : 0 < p' := p'_pos hp hε₀ hε₁ - have : 1 - 8⁻¹ * ε ≤ (∑ i in T, ↑(ν i)) ^ p'⁻¹ := by + have : 1 - 8⁻¹ * ε ≤ (∑ i ∈ T, ↑(ν i)) ^ p'⁻¹ := by rw [← div_le_iff₀, mul_div_assoc, ← div_pow, le_sqrt, mul_pow, ← pow_mul'] at this calc _ ≤ exp (-(8⁻¹ * ε)) := one_sub_le_exp_neg _ @@ -184,10 +184,10 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 _ = 1 + 5 / 8 * ε - 3 / 32 * ε * 1 := by ring _ ≤ 1 + 5 / 8 * ε - 3 / 32 * ε * ε := (sub_le_sub_left (mul_le_mul_of_nonneg_left hε₁ ?_) _) _ = (1 - 8⁻¹ * ε) * (1 + 3 / 4 * ε) := by ring - _ ≤ (∑ i in T, ↑(ν i)) ^ p'⁻¹ * (1 + 3 / 4 * ε) := (mul_le_mul_of_nonneg_right ‹_› ?_) - _ = (∑ i in T, ↑(ν i) * |3 / 4 * ε + 1| ^ p') ^ p'⁻¹ := by + _ ≤ (∑ i ∈ T, ↑(ν i)) ^ p'⁻¹ * (1 + 3 / 4 * ε) := (mul_le_mul_of_nonneg_right ‹_› ?_) + _ = (∑ i ∈ T, ↑(ν i) * |3 / 4 * ε + 1| ^ p') ^ p'⁻¹ := by rw [← sum_mul, mul_rpow, rpow_rpow_inv, abs_of_nonneg, add_comm] <;> positivity - _ ≤ (∑ i in T, ↑(ν i) * |f i + 1| ^ p') ^ p'⁻¹ := + _ ≤ (∑ i ∈ T, ↑(ν i) * |f i + 1| ^ p') ^ p'⁻¹ := rpow_le_rpow ?_ (sum_le_sum fun i hi ↦ mul_le_mul_of_nonneg_left (rpow_le_rpow ?_ (abs_le_abs_of_nonneg ?_ $ add_le_add_right (mem_filter.1 hi).2 _) ?_) ?_) ?_ _ ≤ (∑ i, ↑(ν i) * |f i + 1| ^ p') ^ p'⁻¹ := diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean index 737425e76a..c5498dfb4c 100644 --- a/LeanAPAP/Prereqs/Chang.lean +++ b/LeanAPAP/Prereqs/Chang.lean @@ -95,13 +95,13 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x choose c norm_c hc using fun γ ↦ RCLike.exists_norm_eq_mul_self (dft f γ) have := calc - η * ‖f‖_[1] * #Δ ≤ ∑ γ in Δ, ‖dft f γ‖ := ?_ - _ ≤ ‖∑ x, f x * ∑ γ in Δ, c γ * conj (γ x)‖ := ?_ - _ ≤ ∑ x, ‖f x * ∑ γ in Δ, c γ * conj (γ x)‖ := (norm_sum_le _ _) - _ = ∑ x, ‖f x‖ * ‖∑ γ in Δ, c γ * conj (γ x)‖ := by simp_rw [norm_mul] + η * ‖f‖_[1] * #Δ ≤ ∑ γ ∈ Δ, ‖dft f γ‖ := ?_ + _ ≤ ‖∑ x, f x * ∑ γ ∈ Δ, c γ * conj (γ x)‖ := ?_ + _ ≤ ∑ x, ‖f x * ∑ γ ∈ Δ, c γ * conj (γ x)‖ := (norm_sum_le _ _) + _ = ∑ x, ‖f x‖ * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ := by simp_rw [norm_mul] _ ≤ _ := inner_le_weight_mul_Lp_of_nonneg _ (p := m) ?_ _ _ (fun _ ↦ norm_nonneg _) fun _ ↦ norm_nonneg _ - _ = ‖f‖_[1] ^ (1 - (m : ℝ)⁻¹) * (∑ x, ‖f x‖ * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m) ^ (m⁻¹ : ℝ) := + _ = ‖f‖_[1] ^ (1 - (m : ℝ)⁻¹) * (∑ x, ‖f x‖ * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ (m⁻¹ : ℝ) := by simp_rw [dL1Norm_eq_sum_norm, rpow_natCast] rotate_left · rw [← nsmul_eq_mul'] @@ -127,22 +127,22 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x calc (‖f‖_[1] * (η ^ m * #Δ ^ m)) ^ 2 ≤ (∑ x, ‖f x‖ * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ 2 := by gcongr - _ ≤ (∑ x, ‖f x‖ * sqrt (ν x) * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m) ^ 2 := by + _ ≤ (∑ x, ‖f x‖ * sqrt (ν x) * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ 2 := by gcongr with x; exact hfν _ - _ = (∑ x, ‖f x‖ * (sqrt (ν x) * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m)) ^ 2 := by + _ = (∑ x, ‖f x‖ * (sqrt (ν x) * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m)) ^ 2 := by simp_rw [mul_assoc] - _ ≤ (∑ x, ‖f x‖ ^ 2) * ∑ x, (sqrt (ν x) * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m) ^ 2 := + _ ≤ (∑ x, ‖f x‖ ^ 2) * ∑ x, (sqrt (ν x) * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ 2 := sum_mul_sq_le_sq_mul_sq _ _ _ - _ ≤ ‖f‖_[2] ^ 2 * ∑ x, ν x * (‖∑ γ in Δ, c γ * conj (γ x)‖ ^ 2) ^ m := by + _ ≤ ‖f‖_[2] ^ 2 * ∑ x, ν x * (‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ 2) ^ m := by simp_rw [dL2Norm_sq_eq_sum_norm, mul_pow, sq_sqrt (NNReal.coe_nonneg _), pow_right_comm]; rfl rw [mul_rotate', mul_left_comm, mul_pow, mul_pow, ← pow_mul', ← pow_mul', ← div_le_iff₀', mul_div_assoc, mul_div_assoc] at this calc _ ≤ _ := this _ = ‖(_ : ℂ)‖ := Eq.symm $ RCLike.norm_of_nonneg $ sum_nonneg fun _ _ ↦ by positivity - _ = ‖∑ γ in Δ ^^ m, ∑ δ in Δ ^^ m, + _ = ‖∑ γ ∈ Δ ^^ m, ∑ δ ∈ Δ ^^ m, (∏ i, conj (c (γ i)) * c (δ i)) * conj (dft (fun a ↦ ν a) (∑ i, γ i - ∑ i, δ i))‖ := ?_ - _ ≤ ∑ γ in Δ ^^ m, ∑ δ in Δ ^^ m, + _ ≤ ∑ γ ∈ Δ ^^ m, ∑ δ ∈ Δ ^^ m, ‖(∏ i, conj (c (γ i)) * c (δ i)) * conj (dft (fun a ↦ ν a) (∑ i, γ i - ∑ i, δ i))‖ := (norm_sum_le _ _).trans $ sum_le_sum fun _ _ ↦ norm_sum_le _ _ _ = _ := by simp [energy, norm_c, -Complex.norm_eq_abs, norm_prod] @@ -170,7 +170,7 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) : #Δ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)⌉₊ / η ^ 2⌉₊ ∧ largeSpec f η ⊆ Δ.addSpan := by refine exists_subset_addSpan_card_le_of_forall_addDissociated fun Δ hΔη hΔ ↦ ?_ - obtain hΔ' | hΔ' := @eq_zero_or_pos _ _ #Δ + obtain hΔ' | hΔ' := eq_zero_or_pos #Δ · simp [hΔ'] let α := ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G have : 0 < α := by positivity diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean index 5d4d108705..03622e4109 100644 --- a/LeanAPAP/Prereqs/Energy.lean +++ b/LeanAPAP/Prereqs/Energy.lean @@ -10,7 +10,7 @@ open scoped Nat variable {G : Type*} [AddCommGroup G] {s : Finset G} def energy (n : ℕ) (s : Finset G) (ν : G → ℂ) : ℝ := - ∑ γ in piFinset fun _ : Fin n ↦ s, ∑ δ in piFinset fun _ : Fin n ↦ s, ‖ν (∑ i, γ i - ∑ i, δ i)‖ + ∑ γ ∈ piFinset fun _ : Fin n ↦ s, ∑ δ ∈ piFinset fun _ : Fin n ↦ s, ‖ν (∑ i, γ i - ∑ i, δ i)‖ @[simp] lemma energy_nonneg (n : ℕ) (s : Finset G) (ν : G → ℂ) : 0 ≤ energy n s ν := by diff --git a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean index ae0ee23532..5cfbf4e02b 100644 --- a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean +++ b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean @@ -105,10 +105,10 @@ section CommSemiring variable [CommSemiring β] lemma indicate_inf_apply [Fintype α] (s : Finset ι) (t : ι → Finset α) (x : α) : - 𝟭_[β] (s.inf t) x = ∏ i in s, 𝟭 (t i) x := by simp [indicate_apply, mem_inf, prod_boole] + 𝟭_[β] (s.inf t) x = ∏ i ∈ s, 𝟭 (t i) x := by simp [indicate_apply, mem_inf, prod_boole] lemma indicate_inf [Fintype α] (s : Finset ι) (t : ι → Finset α) : - 𝟭_[β] (s.inf t) = ∏ i in s, 𝟭 (t i) := + 𝟭_[β] (s.inf t) = ∏ i ∈ s, 𝟭 (t i) := funext fun x ↦ by rw [Finset.prod_apply, indicate_inf_apply] variable [StarRing β] 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/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean index f483964126..beb9cee805 100644 --- a/LeanAPAP/Prereqs/NNLpNorm.lean +++ b/LeanAPAP/Prereqs/NNLpNorm.lean @@ -15,11 +15,11 @@ noncomputable def nnLpNorm (f : α → E) (p : ℝ≥0∞) (μ : Measure α) : lemma coe_nnLpNorm_eq_eLpNorm (hf : Memℒp f p μ) : nnLpNorm f p μ = eLpNorm f p μ := by rw [nnLpNorm, ENNReal.coe_toNNReal hf.eLpNorm_ne_top] --- TODO: Rename `eLpNorm_eq_lintegral_rpow_nnnorm` to `eLpNorm_eq_lintegral_nnnorm_rpow_toReal` +-- TODO: Rename `eLpNorm_eq_lintegral_rpow_enorm` to `eLpNorm_eq_lintegral_rpow_enorm_toReal` lemma coe_nnLpNorm_eq_integral_norm_rpow_toReal (hp₀ : p ≠ 0) (hp : p ≠ ∞) - (hf : AEMeasurable (fun x ↦ (‖f x‖₊ : ℝ≥0∞) ^ p.toReal) μ) : + (hf : AEMeasurable (fun x ↦ ‖f x‖ₑ ^ p.toReal) μ) : nnLpNorm f p μ = (∫ x, ‖f x‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹ := by - rw [nnLpNorm, eLpNorm_eq_lintegral_rpow_nnnorm hp₀ hp, ENNReal.coe_toNNReal_eq_toReal, + rw [nnLpNorm, eLpNorm_eq_lintegral_rpow_enorm hp₀ hp, ENNReal.coe_toNNReal_eq_toReal, ← ENNReal.toReal_rpow, ← integral_toReal hf] simp [← ENNReal.toReal_rpow] · exact .of_forall fun x ↦ ENNReal.rpow_lt_top_of_nonneg (by positivity) (by simp) @@ -30,7 +30,7 @@ lemma coe_nnLpNorm_nnreal_eq_integral_norm_rpow {p : ℝ≥0} (hp : p ≠ 0) nnLpNorm f p μ = (∫ x, ‖f x‖ ^ (p : ℝ) ∂μ) ^ (p⁻¹ : ℝ) := by rw [coe_nnLpNorm_eq_integral_norm_rpow_toReal (by positivity) (by simp) hf]; simp -lemma coe_nnLpNorm_one_eq_integral_norm (hf : AEMeasurable (fun x ↦ ‖f x‖₊) μ) : +lemma coe_nnLpNorm_one_eq_integral_norm (hf : AEMeasurable (fun x ↦ ‖f x‖ₑ) μ) : nnLpNorm f 1 μ = ∫ x, ‖f x‖ ∂μ := by rw [coe_nnLpNorm_eq_integral_norm_rpow_toReal one_ne_zero ENNReal.coe_ne_top (by simpa using hf)] simp 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/docbuild/lake-manifest.json b/docbuild/lake-manifest.json index f58587e66b..d8bcaca785 100644 --- a/docbuild/lake-manifest.json +++ b/docbuild/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "0291556f04e89d46cd2999f0f4c1164c81778207", + "rev": "e9d995eaa95a4e3c880ffe94c416c34113e0f251", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}, {"type": "path", @@ -32,7 +32,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "470c41643209208d325a5a7315116f293c7443fb", + "rev": "b64b8eab8cfcf24c398e84b11c77b6555b61095a", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -42,7 +42,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "46376bc3c8f46ac1a1fd7712856b0f7bd6166098", + "rev": "9e99cb8cd9ba6906472634e6973c7e27482a70bb", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -52,7 +52,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "f8ed91f3a9d806648ae6a03ab98c8b87e8bedc7e", + "rev": "26b1d510d9b5238d36b521d5367c707146fecd9d", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -62,7 +62,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9082fa7b9f7bcad5b4b6052a629eb9347580073a", + "rev": "8f1b0576c3aeb2851403b6f5dd56a5ee53e705de", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -72,10 +72,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35", + "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0-rc1", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -92,47 +92,47 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377", + "rev": "f72319c9686788305a8ab059f3c4d8c724785c83", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0-rc1", + "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": "a4a08d92be3de00def5298059bf707c72dfd3c66", + "rev": "79402ad9ab4be9a2286701a9880697e2351e4955", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac", + "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "v4.15.0", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd", + "rev": "43dc9fd41505ba34dd359550c94706b4f4abefec", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml index cea023c197..6da197f74d 100644 --- a/docbuild/lakefile.toml +++ b/docbuild/lakefile.toml @@ -10,4 +10,4 @@ path = "../" [[require]] scope = "leanprover" name = "doc-gen4" -rev = "v4.15.0" +rev = "main" diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain index cf25a9816f..2ffc30ceba 100644 --- a/docbuild/lean-toolchain +++ b/docbuild/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0-rc1 +leanprover/lean4:v4.16.0-rc2 \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json index c03bcbc0fb..89619b920a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,20 +5,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608", + "rev": "8f1b0576c3aeb2851403b6f5dd56a5ee53e705de", "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": "43dc9fd41505ba34dd359550c94706b4f4abefec", "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