From 5c16c6a9a8bb45be40bdd773f0d2f09310c03773 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 4 Nov 2024 10:53:07 +0000 Subject: [PATCH] Bump mathlib --- LeanAPAP/Physics/AlmostPeriodicity.lean | 2 +- LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean | 157 +++++++++++---------- lake-manifest.json | 22 +-- lean-toolchain | 2 +- 4 files changed, 93 insertions(+), 90 deletions(-) diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index 9f010181f7..8f8fdc9d79 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -252,7 +252,7 @@ variable [DiscreteMeasurableSpace G] lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) : (8 * m) ^ m * k ^ (m - 1) * ∑ a ∈ A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤ - (8 * m) ^ m * k ^ (m - 1) * ∑ a ∈ A ^^ k, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := by + (8 * m) ^ m * k ^ (m - 1) * ∑ _a ∈ A ^^ k, ∑ _i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := by -- lots of the equalities about m can be automated but it's *way* slower have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two] have hm' : 1 < 2 * m := (Nat.mul_le_mul_left 2 hm).trans_lt' $ by norm_num1 diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean index a1d3d70b3a..7ed8dd2b6a 100644 --- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean +++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean @@ -1,6 +1,6 @@ /- Copyright (c) 2023 Yaël Dillies, Bhavik Mehta. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. +Released under Apache 2.0 license as described ∈ the file LICENSE. Authors: Yaël Dillies, Bhavik Mehta -/ import Mathlib.Algebra.Order.Chebyshev @@ -20,32 +20,32 @@ variable {ι : Type*} {A : Finset ι} {m n : ℕ} local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s private lemma step_one (hA : A.Nonempty) (f : ι → ℝ) (a : Fin n → ι) - (hf : ∀ i, ∑ a in A ^^ n, f (a i) = 0) : + (hf : ∀ i, ∑ a ∈ A ^^ n, f (a i) = 0) : |∑ i, f (a i)| ^ (m + 1) ≤ - (∑ b in A ^^ n, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / #A ^ n := by + (∑ b ∈ A ^^ n, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / #A ^ n := by let B := A ^^ n calc |∑ i, f (a i)| ^ (m + 1) - = |∑ i, (f (a i) - (∑ b in B, f (b i)) / #B)| ^ (m + 1) := by + = |∑ i, (f (a i) - (∑ b ∈ B, f (b i)) / #B)| ^ (m + 1) := by simp only [hf, sub_zero, zero_div] - _ = |(∑ b in B, ∑ i, (f (a i) - f (b i))) / #B| ^ (m + 1) := by + _ = |(∑ 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, Finset.card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀] positivity - _ = |∑ b in B, ∑ i, (f (a i) - f (b i))| ^ (m + 1) / #B ^ (m + 1) := by + _ = |∑ b ∈ B, ∑ i, (f (a i) - f (b i))| ^ (m + 1) / #B ^ (m + 1) := by rw [abs_div, div_pow, Nat.abs_cast] - _ ≤ (∑ b in B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / #B ^ (m + 1) := by + _ ≤ (∑ b ∈ B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / #B ^ (m + 1) := by gcongr; exact IsAbsoluteValue.abv_sum _ _ _ - _ = (∑ b in B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / #B ^ m / #B := by + _ = (∑ b ∈ B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / #B ^ m / #B := by rw [div_div, ← _root_.pow_succ] - _ ≤ (∑ b in B, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / #B := by + _ ≤ (∑ b ∈ B, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / #B := by gcongr; exact pow_sum_div_card_le_sum_pow (fun _ _ ↦ abs_nonneg _) _ _ = _ := by simp [B] -private lemma step_one' (hA : A.Nonempty) (f : ι → ℝ) (hf : ∀ i, ∑ a in A ^^ n, f (a i) = 0) (m : ℕ) +private lemma step_one' (hA : A.Nonempty) (f : ι → ℝ) (hf : ∀ i, ∑ a ∈ A ^^ n, f (a i) = 0) (m : ℕ) (a : Fin n → ι) : - |∑ i, f (a i)| ^ m ≤ (∑ b in A ^^ n, |∑ i, (f (a i) - f (b i))| ^ m) / #A ^ n := by + |∑ i, f (a i)| ^ m ≤ (∑ b ∈ A ^^ n, |∑ i, (f (a i) - f (b i))| ^ m) / #A ^ n := by cases m · simp only [_root_.pow_zero, sum_const, prod_const, Nat.smul_one_eq_cast, Finset.card_fin, card_piFinset, ← Nat.cast_pow] @@ -58,15 +58,15 @@ private lemma step_one' (hA : A.Nonempty) (f : ι → ℝ) (hf : ∀ i, ∑ a in -- private lemma step_two_aux' {β γ : Type*} [AddCommMonoid β] [CommRing γ] -- (f : (Fin n → ι) → (Fin n → γ)) (ε : Fin n → γ) -- (hε : ∀ i, ε i = -1 ∨ ε i = 1) (g : (Fin n → γ) → β) : --- ∑ a b in A ^^ n, g (ε * (f a - f b)) = ∑ a b in A ^^ n, g (f a - f b) := +-- ∑ a b ∈ A ^^ n, g (ε * (f a - f b)) = ∑ a b ∈ A ^^ n, g (f a - f b) := -- feels like could generalise more... -- the key point is that you combine the double sums into a single sum, and do a pair swap -- when the corresponding ε is -1 -- but the order here is a bit subtle (ie this explanation is an oversimplification) private lemma step_two_aux (A : Finset ι) (f : ι → ℝ) (ε : Fin n → ℝ) (hε : ε ∈ ({-1, 1} : Finset ℝ)^^n) (g : (Fin n → ℝ) → ℝ) : - ∑ a in A ^^ n, ∑ b in A ^^ n, g (ε * (f ∘ a - f ∘ b)) = - ∑ a in A ^^ n, ∑ b in A ^^ n, g (f ∘ a - f ∘ b) := by + ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, g (ε * (f ∘ a - f ∘ b)) = + ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, g (f ∘ a - f ∘ b) := by rw [← sum_product', ← sum_product'] let swapper : (Fin n → ι) × (Fin n → ι) → (Fin n → ι) × (Fin n → ι) := by intro xy @@ -90,13 +90,13 @@ private lemma step_two_aux (A : Finset ι) (f : ι → ℝ) (ε : Fin n → ℝ) ring private lemma step_two (f : ι → ℝ) : - ∑ a in A ^^ n, ∑ b in A ^^ n, (∑ i, (f (a i) - f (b i))) ^ (2 * m) = - 2⁻¹ ^ n * ∑ ε in ({-1, 1} : Finset ℝ)^^n, - ∑ a in A ^^ n, ∑ b in A ^^ n, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m) := by + ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, (∑ i, (f (a i) - f (b i))) ^ (2 * m) = + 2⁻¹ ^ n * ∑ ε ∈ ({-1, 1} : Finset ℝ)^^n, + ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m) := by let B := A ^^ n have : ∀ ε ∈ ({-1, 1} : Finset ℝ)^^n, - ∑ a in B, ∑ b in B, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m) = - ∑ a in B, ∑ b in B, (∑ i, (f (a i) - f (b i))) ^ (2 * m) := + ∑ a ∈ B, ∑ b ∈ B, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m) = + ∑ a ∈ B, ∑ b ∈ B, (∑ i, (f (a i) - f (b i))) ^ (2 * m) := fun ε hε ↦ step_two_aux A f _ hε fun z : Fin n → ℝ ↦ univ.sum z ^ (2 * m) rw [Finset.sum_congr rfl this, sum_const, card_piFinset_const, card_pair, nsmul_eq_mul, Nat.cast_pow, Nat.cast_two, inv_pow, inv_mul_cancel_left₀] @@ -104,11 +104,11 @@ private lemma step_two (f : ι → ℝ) : · norm_num private lemma step_three (f : ι → ℝ) : - ∑ ε in ({-1, 1} : Finset ℝ)^^n, - ∑ a in A ^^ n, ∑ b in A ^^ n, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m) = - ∑ a in A ^^ n, ∑ b in A ^^ n, ∑ k in piAntidiag univ (2 * m), + ∑ ε ∈ ({-1, 1} : Finset ℝ)^^n, + ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m) = + ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, ∑ k ∈ piAntidiag univ (2 * m), (multinomial univ k * ∏ t, (f (a t) - f (b t)) ^ k t) * - ∑ ε in ({-1, 1} : Finset ℝ)^^n, ∏ t, ε t ^ k t := by + ∑ ε ∈ ({-1, 1} : Finset ℝ)^^n, ∏ t, ε t ^ k t := by simp only [@sum_comm _ _ (Fin n → ℝ) _ _ (A ^^ n), ← Complex.abs_pow, sum_pow_eq_sum_piAntidiag] refine sum_congr rfl fun a _ ↦ ?_ refine sum_congr rfl fun b _ ↦ ?_ @@ -117,23 +117,17 @@ private lemma step_three (f : ι → ℝ) : rw [← mul_assoc, mul_right_comm] private lemma step_four {k : Fin n → ℕ} : - ∑ ε in ({-1, 1} : Finset ℝ)^^n, ∏ t, ε t ^ k t = 2 ^ n * ite (∀ i, Even (k i)) 1 0 := by - have := sum_prod_piFinset ({-1, 1} : Finset ℝ) fun i fi ↦ fi ^ k i - rw [this, ← Fintype.prod_boole] - have : (2 : ℝ) ^ n = ∏ i : Fin n, 2 := by simp - rw [this, ← prod_mul_distrib] - refine prod_congr rfl fun t _ ↦ ?_ - rw [sum_pair, one_pow, mul_boole] - swap - · norm_num - split_ifs with h - · rw [h.neg_one_pow, one_add_one_eq_two] - rw [Nat.not_even_iff_odd] at h - simp [h.neg_one_pow] + ∑ ε ∈ ({-1, 1} : Finset ℝ)^^n, ∏ t, ε t ^ k t = 2 ^ n * ite (∀ i, Even (k i)) 1 0 := by + calc + _ = ∏ i, ∑ j ∈ ({-1, 1} : Finset ℝ), j ^ k i := by rw [← sum_prod_piFinset] + _ = ∏ i, if Even (k i) then 2 else 0 := by + congr with i + split_ifs <;> simp_all [sum_pair (show (-1 : ℝ) ≠ 1 by norm_num), one_add_one_eq_two] + _ = _ := by simp [Fintype.prod_ite_zero] -- double_multinomial private lemma step_six {f : ι → ℝ} {a b : Fin n → ι} : - ∑ k : Fin n → ℕ in piAntidiag univ m, + ∑ k ∈ piAntidiag univ m, (multinomial univ fun a ↦ 2 * k a : ℝ) * ∏ i, (f (a i) - f (b i)) ^ (2 * k i) ≤ m ^ m * (∑ i, (f (a i) - f (b i)) ^ 2) ^ m := by rw [sum_pow_eq_sum_piAntidiag, mul_sum] @@ -161,14 +155,14 @@ private lemma step_eight {f : ι → ℝ} {a b : Fin n → ι} : refine add_pow_le ?_ ?_ m <;> positivity private lemma end_step {f : ι → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) : - (∑ a in A ^^ n, ∑ b in A ^^ n, ∑ k in piAntidiag univ m, + (∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, ∑ k ∈ piAntidiag univ m, ↑(multinomial univ fun i ↦ 2 * k i) * ∏ t, (f (a t) - f (b t)) ^ (2 * k t)) / #A ^ n - ≤ (4 * m) ^ m * ∑ a in A ^^ n, (∑ i, f (a i) ^ 2) ^ m := by + ≤ (4 * m) ^ m * ∑ a ∈ A ^^ n, (∑ i, f (a i) ^ 2) ^ m := by let B := A ^^ n calc - (∑ a in B, ∑ b in B, ∑ k : Fin n → ℕ in piAntidiag univ m, + (∑ a ∈ B, ∑ b ∈ B, ∑ k ∈ piAntidiag univ m, (multinomial univ fun i ↦ 2 * k i : ℝ) * ∏ t, (f (a t) - f (b t)) ^ (2 * k t)) / #A ^ n - _ ≤ (∑ a in B, ∑ b in B, m ^ m * 2 ^ (m + (m - 1)) * + _ ≤ (∑ a ∈ B, ∑ b ∈ B, m ^ m * 2 ^ (m + (m - 1)) * ((∑ i, f (a i) ^ 2) ^ m + (∑ i, f (b i) ^ 2) ^ m) : ℝ) / #A ^ n := by gcongr; exact step_six.trans $ step_seven.trans step_eight _ = _ := by @@ -181,11 +175,13 @@ private lemma end_step {f : ι → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) : namespace Real +attribute [-instance] decidableForallFin + /-- The **Marcinkiewicz-Zygmund inequality** for real-valued functions, with a slightly better constant than `Real.marcinkiewicz_zygmund`. -/ -theorem marcinkiewicz_zygmund' (m : ℕ) (f : ι → ℝ) (hf : ∀ i, ∑ a in A ^^ n, f (a i) = 0) : - ∑ a in A ^^ n, (∑ i, f (a i)) ^ (2 * m) ≤ - (4 * m) ^ m * ∑ a in A ^^ n, (∑ i, f (a i) ^ 2) ^ m := by +theorem marcinkiewicz_zygmund' (m : ℕ) (f : ι → ℝ) (hf : ∀ i, ∑ a ∈ A ^^ n, f (a i) = 0) : + ∑ a ∈ A ^^ n, (∑ i, f (a i)) ^ (2 * m) ≤ + (4 * m) ^ m * ∑ a ∈ A ^^ n, (∑ i, f (a i) ^ 2) ^ m := by obtain rfl | hm := m.eq_zero_or_pos · simp have hm' : 1 ≤ m := by rwa [Nat.succ_le_iff] @@ -193,38 +189,45 @@ theorem marcinkiewicz_zygmund' (m : ℕ) (f : ι → ℝ) (hf : ∀ i, ∑ a in · cases n <;> cases m <;> simp let B := A ^^ n calc - ∑ a in B, (∑ i, f (a i)) ^ (2 * m) - ≤ ∑ a in A ^^ n, (∑ b in B, |∑ i, (f (a i) - f (b i))| ^ (2 * m))/ #A ^ n := by + ∑ a ∈ B, (∑ i, f (a i)) ^ (2 * m) + ≤ ∑ a ∈ A ^^ n, (∑ b ∈ B, |∑ i, (f (a i) - f (b i))| ^ (2 * m)) / #A ^ n := by gcongr; simpa [pow_mul, sq_abs] using step_one' hA f hf (2 * m) _ - _ ≤ _ := ?_ - rw [← sum_div] - simp only [pow_mul, sq_abs] - simp only [← pow_mul] - rw [step_two, step_three, mul_comm, inv_pow, ← div_eq_mul_inv, div_div] - simp only [step_four, mul_ite, mul_zero, mul_one, ← sum_filter, ← sum_mul] - rw [mul_comm, mul_div_mul_left] - swap; · positivity - simpa only [even_iff_two_dvd, ← map_nsmul_piAntidiag_univ _ two_ne_zero, sum_map, - Function.Embedding.coeFn_mk] using end_step hm' hA + _ = (∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, ∑ k ∈ piAntidiag univ (2 * m) with ∀ i, 2 ∣ k i, + multinomial univ (fun i ↦ k i) * ∏ t, (f (a t) - f (b t)) ^ k t) / #A ^ n := by + rw [← sum_div] + simp only [pow_mul, sq_abs] + simp only [← pow_mul] + rw [step_two, step_three, mul_comm, inv_pow, ← div_eq_mul_inv, div_div] + simp only [step_four, mul_ite, mul_zero, mul_one, ← sum_filter, ← sum_mul, even_iff_two_dvd] + rw [mul_comm, mul_div_mul_left] + positivity + _ = (∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, ∑ k ∈ (piAntidiag univ m).map + ⟨(2 • ·), fun _ _ h ↦ funext fun i ↦ mul_right_injective₀ two_ne_zero (congr_fun h i)⟩, + multinomial univ (fun i ↦ k i) * ∏ t, (f (a t) - f (b t)) ^ k t) / #A ^ n := by + rw [map_nsmul_piAntidiag_univ m (ι := Fin n) (n := 2) two_ne_zero] + _ = (∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, ∑ k ∈ piAntidiag univ m, + multinomial univ (fun i ↦ 2 * k i) * ∏ t, (f (a t) - f (b t)) ^ (2 * k t)) / #A ^ n := by + simp + _ ≤ _ := end_step hm' hA /-- The **Marcinkiewicz-Zygmund inequality** for real-valued functions, with a slightly easier to bound constant than `Real.marcinkiewicz_zygmund'`. Note that `RCLike.marcinkiewicz_zygmund` is another version that works for both `ℝ` and `ℂ` at the expense of a slightly worse constant. -/ -theorem marcinkiewicz_zygmund (hm : m ≠ 0) (f : ι → ℝ) (hf : ∀ i, ∑ a in A ^^ n, f (a i) = 0) : - ∑ a in A ^^ n, (∑ i, f (a i)) ^ (2 * m) ≤ - (4 * m) ^ m * n ^ (m - 1) * ∑ a in A ^^ n, ∑ i, f (a i) ^ (2 * m) := by +theorem marcinkiewicz_zygmund (hm : m ≠ 0) (f : ι → ℝ) (hf : ∀ i, ∑ a ∈ A ^^ n, f (a i) = 0) : + ∑ a ∈ A ^^ n, (∑ i, f (a i)) ^ (2 * m) ≤ + (4 * m) ^ m * n ^ (m - 1) * ∑ a ∈ A ^^ n, ∑ i, f (a i) ^ (2 * m) := by obtain _ | m := m · simp at hm obtain rfl | hn := n.eq_zero_or_pos · simp calc - ∑ a in A ^^ n, (∑ i, f (a i)) ^ (2 * (m + 1)) - ≤ (4 * ↑(m + 1)) ^ (m + 1) * ∑ a in A ^^ n, (∑ i, f (a i) ^ 2) ^ (m + 1) := + ∑ a ∈ A ^^ n, (∑ i, f (a i)) ^ (2 * (m + 1)) + ≤ (4 * ↑(m + 1)) ^ (m + 1) * ∑ a ∈ A ^^ n, (∑ i, f (a i) ^ 2) ^ (m + 1) := marcinkiewicz_zygmund' _ f hf - _ ≤ (4 * ↑(m + 1)) ^ (m + 1) * (∑ a in A ^^ n, n ^ m * ∑ i, f (a i) ^ (2 * (m + 1))) := ?_ - _ ≤ (4 * ↑(m + 1)) ^ (m + 1) * n ^ m * ∑ a in A ^^ n, ∑ i, f (a i) ^ (2 * (m + 1)) := by + _ ≤ (4 * ↑(m + 1)) ^ (m + 1) * (∑ a ∈ A ^^ n, n ^ m * ∑ i, f (a i) ^ (2 * (m + 1))) := ?_ + _ ≤ (4 * ↑(m + 1)) ^ (m + 1) * n ^ m * ∑ a ∈ A ^^ n, ∑ i, f (a i) ^ (2 * (m + 1)) := by simp_rw [mul_assoc, mul_sum]; rfl gcongr with a rw [← div_le_iff₀'] @@ -238,36 +241,36 @@ namespace RCLike variable {𝕜 : Type*} [RCLike 𝕜] /-- The **Marcinkiewicz-Zygmund inequality** for real- or complex-valued functions. -/ -lemma marcinkiewicz_zygmund (hm : m ≠ 0) (f : ι → 𝕜) (hf : ∀ i, ∑ a in A ^^ n, f (a i) = 0) : - ∑ a in A ^^ n, ‖∑ i, f (a i)‖ ^ (2 * m) ≤ - (8 * m) ^ m * n ^ (m - 1) * ∑ a in A ^^ n, ∑ i, ‖f (a i)‖ ^ (2 * m) := by +lemma marcinkiewicz_zygmund (hm : m ≠ 0) (f : ι → 𝕜) (hf : ∀ i, ∑ a ∈ A ^^ n, f (a i) = 0) : + ∑ a ∈ A ^^ n, ‖∑ i, f (a i)‖ ^ (2 * m) ≤ + (8 * m) ^ m * n ^ (m - 1) * ∑ a ∈ A ^^ n, ∑ i, ‖f (a i)‖ ^ (2 * m) := by let f₁ x : ℝ := re (f x) let f₂ x : ℝ := im (f x) let B := A ^^ n - have hf₁ i : ∑ a in B, f₁ (a i) = 0 := by rw [← map_sum, hf, map_zero] - have hf₂ i : ∑ a in B, f₂ (a i) = 0 := by rw [← map_sum, hf, map_zero] + have hf₁ i : ∑ a ∈ B, f₁ (a i) = 0 := by rw [← map_sum, hf, map_zero] + have hf₂ i : ∑ a ∈ B, f₂ (a i) = 0 := by rw [← map_sum, hf, map_zero] have h₁ := Real.marcinkiewicz_zygmund hm _ hf₁ have h₂ := Real.marcinkiewicz_zygmund hm _ hf₂ simp only [pow_mul, RCLike.norm_sq_eq_def] simp only [← sq, map_sum, map_sum] calc - ∑ a in B, ((∑ i, re (f (a i))) ^ 2 + (∑ i, im (f (a i))) ^ 2) ^ m ≤ - ∑ a in B, + ∑ a ∈ B, ((∑ i, re (f (a i))) ^ 2 + (∑ i, im (f (a i))) ^ 2) ^ m ≤ + ∑ a ∈ B, 2 ^ (m - 1) * (((∑ i, re (f (a i))) ^ 2) ^ m + ((∑ i, im (f (a i))) ^ 2) ^ m) := by gcongr with a; apply add_pow_le <;> positivity - _ = 2 ^ (m - 1) * (∑ a in B, (∑ i, re (f (a i))) ^ (2 * m) + - ∑ a in B, (∑ i, im (f (a i))) ^ (2 * m)) := by + _ = 2 ^ (m - 1) * (∑ a ∈ B, (∑ i, re (f (a i))) ^ (2 * m) + + ∑ a ∈ B, (∑ i, im (f (a i))) ^ (2 * m)) := by simp only [← sum_add_distrib, mul_sum, pow_mul] _ ≤ 2 ^ (m - 1) * ((4 * m) ^ m * n ^ (m - 1) * - ∑ a in B, ∑ i, re (f (a i)) ^ (2 * m) + (4 * m) ^ m * n ^ (m - 1) * - ∑ a in B, ∑ i, im (f (a i)) ^ (2 * m)) := by gcongr + ∑ a ∈ B, ∑ i, re (f (a i)) ^ (2 * m) + (4 * m) ^ m * n ^ (m - 1) * + ∑ a ∈ B, ∑ i, im (f (a i)) ^ (2 * m)) := by gcongr _ = 2 ^ (m - 1) * ((4 * m) ^ m * n ^ (m - 1) * - ∑ a in B, ∑ i, (re (f (a i)) ^ (2 * m) + im (f (a i)) ^ (2 * m))) := by + ∑ a ∈ B, ∑ i, (re (f (a i)) ^ (2 * m) + im (f (a i)) ^ (2 * m))) := by simp_rw [sum_add_distrib, mul_add] _ ≤ 2 ^ (m - 1) * ((4 * m) ^ m * n ^ (m - 1) * - ∑ a in B, ∑ i, 2 * (re (f (a i)) ^ 2 + im (f (a i)) ^ 2) ^ m) := by + ∑ a ∈ B, ∑ i, 2 * (re (f (a i)) ^ 2 + im (f (a i)) ^ 2) ^ m) := by simp_rw [pow_mul]; gcongr; apply pow_add_pow_le' <;> positivity - _ = (8 * m) ^ m * n ^ (m - 1) * ∑ a in B, ∑ i, (re (f (a i)) ^ 2 + im (f (a i)) ^ 2) ^ m := by + _ = (8 * m) ^ m * n ^ (m - 1) * ∑ a ∈ B, ∑ i, (re (f (a i)) ^ 2 + im (f (a i)) ^ 2) ^ m := by simp_rw [← mul_sum, show (8 : ℝ) = 2 * 4 by norm_num, mul_pow, ← pow_sub_one_mul hm (2 : ℝ)] ring diff --git a/lake-manifest.json b/lake-manifest.json index 4962f020d8..f54081215c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18", + "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785", + "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46", + "rev": "45d016d59cf45bcf8493a203e9564cfec5203d9b", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,17 +35,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "23268f52d3505955de3c26a42032702c25cfcbf8", + "rev": "1383e72b40dd62a566896a6e348ffe868801b172", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.44", + "inputRev": "v0.0.46", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", + "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb", + "rev": "ac7b989cbf99169509433124ae484318e953d201", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d212dd74414e997653cd3484921f4159c955ccca", + "rev": "0f1430e6f1193929f13905d450b2a44a54f3927e", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "df174a8a32fb9b7661ec4faa48a6a6a6bb4cf0d5", + "rev": "88fac4fdcd3f426be4d972e0d3a7c78458e0bf01", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -105,7 +105,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "107e98b3e7603628d9bfd817b4704488d8a25e96", + "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -125,7 +125,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "c2156beadb1a4d049ff3b19fe396c5403025aac5", + "rev": "b6ae1cf11e83d972ffa363f9cdc8a2f89aaa24dc", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 4f86f953fb..0bef727630 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.13.0 +leanprover/lean4:v4.14.0-rc1