From 5c366386f8365a3431f83e78dc89846fda82ea65 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 29 Oct 2024 09:44:04 +0000 Subject: [PATCH] Bump mathlib --- LeanAPAP/Extras/BSG.lean | 333 ++++++++---------- LeanAPAP/FiniteField.lean | 8 +- LeanAPAP/Integer.lean | 2 +- LeanAPAP/Physics/AlmostPeriodicity.lean | 113 +++--- LeanAPAP/Physics/DRC.lean | 64 ++-- LeanAPAP/Physics/Unbalancing.lean | 6 +- .../Prereqs/AddChar/PontryaginDuality.lean | 2 +- LeanAPAP/Prereqs/Bohr/Basic.lean | 6 +- LeanAPAP/Prereqs/Chang.lean | 20 +- .../Prereqs/Convolution/Discrete/Basic.lean | 16 +- LeanAPAP/Prereqs/Convolution/ThreeAP.lean | 4 +- LeanAPAP/Prereqs/Energy.lean | 4 +- .../Prereqs/FourierTransform/Discrete.lean | 2 +- .../Prereqs/Function/Indicator/Basic.lean | 2 +- LeanAPAP/Prereqs/Function/Indicator/Defs.lean | 16 +- LeanAPAP/Prereqs/LargeSpec.lean | 2 +- LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean | 20 +- LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean | 24 +- lake-manifest.json | 12 +- 19 files changed, 313 insertions(+), 343 deletions(-) diff --git a/LeanAPAP/Extras/BSG.lean b/LeanAPAP/Extras/BSG.lean index 7e0944f75a..b8fbeebf82 100644 --- a/LeanAPAP/Extras/BSG.lean +++ b/LeanAPAP/Extras/BSG.lean @@ -1,5 +1,6 @@ import Mathlib.Combinatorics.Additive.Energy import Mathlib.Data.Real.StarOrdered +import Mathlib.Tactic.Positivity.Finset import LeanAPAP.Prereqs.Convolution.Discrete.Basic import LeanAPAP.Prereqs.Convolution.Order @@ -10,73 +11,66 @@ section variable {α : Type*} [DecidableEq α] {H : Finset (α × α)} {A B X : Finset α} {x : α} private noncomputable def oneOfPair (H : Finset (α × α)) (X : Finset α) : Finset α := - X.filter fun x ↦ (3 / 4 : ℝ) * X.card ≤ (H.filter fun yz ↦ yz.1 = x).card + {x ∈ X | (3 / 4 : ℝ) * #X ≤ #{yz ∈ H | yz.1 = x}} private lemma oneOfPair_mem : - x ∈ oneOfPair H X ↔ x ∈ X ∧ (3 / 4 : ℝ) * X.card ≤ (H.filter fun yz ↦ yz.1 = x).card := - mem_filter + x ∈ oneOfPair H X ↔ x ∈ X ∧ (3 / 4 : ℝ) * #X ≤ #{yz ∈ H | yz.1 = x} := mem_filter -private lemma oneOfPair_mem' (hH : H ⊆ X ×ˢ X) : - (H.filter fun yz ↦ yz.1 = x).card = (X.filter fun c ↦ (x, c) ∈ H).card := by +private lemma oneOfPair_mem' (hH : H ⊆ X ×ˢ X) : #{yz ∈ H | yz.1 = x} = #{c ∈ X | (x, c) ∈ H} := by refine card_nbij' Prod.snd (fun c ↦ (x, c)) ?_ (by simp) (by aesop) (by simp) simp (config := { contextual := true }) only [eq_comm, Prod.forall, mem_filter, and_imp, and_true] exact fun a b hab _ ↦ (mem_product.1 (hH hab)).2 private lemma oneOfPair_bound_one : - ∑ x in X \ oneOfPair H X, ((H.filter (fun xy ↦ xy.1 = x)).card : ℝ) ≤ (3 / 4) * X.card ^ 2 := - calc _ ≤ ∑ _x in X \ oneOfPair H X, (3 / 4 : ℝ) * X.card := sum_le_sum fun i hi ↦ by - simp only [oneOfPair, ← filter_not, Prod.forall, not_le, not_lt, mem_filter] at hi - exact hi.2.le - _ = (X \ oneOfPair H X).card * ((3 / 4 : ℝ) * X.card) := by simp - _ ≤ X.card * ((3 / 4 : ℝ) * X.card) := by gcongr; exact sdiff_subset + ∑ x ∈ X \ oneOfPair H X, (#{yz ∈ H | yz.1 = x} : ℝ) ≤ (3 / 4) * #X ^ 2 := + calc _ ≤ ∑ _x ∈ X \ oneOfPair H X, (3 / 4 : ℝ) * #X := by + gcongr with i hi + simp only [oneOfPair, ← filter_not, Prod.forall, not_le, not_lt, mem_filter] at hi + exact hi.2.le + _ = #(X \ oneOfPair H X) * ((3 / 4 : ℝ) * #X) := by simp + _ ≤ #X * ((3 / 4 : ℝ) * #X) := by gcongr; exact sdiff_subset _ = _ := by ring -private lemma oneOfPair_bound_two (hH : H ⊆ X ×ˢ X) (Hcard : (7 / 8 : ℝ) * X.card ^ 2 ≤ H.card) : - (1 / 8 : ℝ) * X.card ^ 2 ≤ X.card * (oneOfPair H X).card := - calc _ = (7 / 8 : ℝ) * X.card ^ 2 - 3 / 4 * X.card ^ 2 := by ring - _ ≤ H.card - (3 / 4 : ℝ) * X.card ^ 2 := by linarith - _ ≤ H.card - ∑ x in X \ oneOfPair H X, ↑(H.filter (fun xy ↦ xy.1 = x)).card := - sub_le_sub_left oneOfPair_bound_one _ - _ = (H.card - ∑ x in X, ↑(H.filter (fun xy ↦ xy.1 = x)).card) + - ∑ x in oneOfPair H X, ↑(H.filter (fun xy ↦ xy.1 = x)).card := by - rw [sum_sdiff_eq_sub, sub_add] - exact filter_subset _ _ - _ = ∑ x in oneOfPair H X, ↑(H.filter (fun xy ↦ xy.1 = x)).card := by - rw [add_left_eq_self, sub_eq_zero, ← Nat.cast_sum, Nat.cast_inj, - ← card_eq_sum_card_fiberwise] - intro x hx - exact (mem_product.1 (hH hx)).1 - _ ≤ ∑ _x in oneOfPair H X, ↑X.card := sum_le_sum <| fun i hi ↦ Nat.cast_le.2 <| by - rw [oneOfPair_mem' hH] - exact card_le_card (filter_subset _ _) - _ = X.card * (oneOfPair H X).card := by simp [mul_comm] - -private lemma oneOfPair_bound {K : ℝ} (hH : H ⊆ X ×ˢ X) (hX : (0 : ℝ) < X.card) - (Hcard : (7 / 8 : ℝ) * X.card ^ 2 ≤ H.card) (h : A.card / (2 * K) ≤ X.card) : - A.card / (2 ^ 4 * K) ≤ (oneOfPair H X).card := -- by - calc _ = (A.card / (2 * K)) / 8 := by ring - _ ≤ (X.card / 8 : ℝ) := by gcongr - _ ≤ (oneOfPair H X).card := - le_of_mul_le_mul_left ((oneOfPair_bound_two hH Hcard).trans_eq' (by ring)) hX +private lemma oneOfPair_bound_two (hH : H ⊆ X ×ˢ X) (Hcard : (7 / 8 : ℝ) * #X ^ 2 ≤ #H) : + (1 / 8 : ℝ) * #X ^ 2 ≤ #X * #(oneOfPair H X) := + calc _ = (7 / 8 : ℝ) * #X ^ 2 - 3 / 4 * #X ^ 2 := by ring + _ ≤ #H - (3 / 4 : ℝ) * #X ^ 2 := by linarith + _ ≤ #H - ∑ x ∈ X \ oneOfPair H X, (#{yz ∈ H | yz.1 = x} : ℝ) := by + gcongr; exact oneOfPair_bound_one + _ = #H - ∑ x ∈ X, (#{yz ∈ H | yz.1 = x} : ℝ) + + ∑ x ∈ oneOfPair H X, (#{yz ∈ H | yz.1 = x} : ℝ) := by + rw [sum_sdiff_eq_sub, sub_add]; exact filter_subset .. + _ = ∑ x ∈ oneOfPair H X, (#{yz ∈ H | yz.1 = x} : ℝ) := by + rw [add_left_eq_self, sub_eq_zero, ← Nat.cast_sum, Nat.cast_inj, + ← card_eq_sum_card_fiberwise] + exact fun x hx ↦ (mem_product.1 (hH hx)).1 + _ ≤ ∑ _x ∈ oneOfPair H X, (#X : ℝ) := by + simp_rw [oneOfPair_mem' hH]; gcongr with i; exact filter_subset .. + _ = #X * #(oneOfPair H X) := by simp [mul_comm] + +private lemma oneOfPair_bound {K : ℝ} (hH : H ⊆ X ×ˢ X) (hX : (0 : ℝ) < #X) + (Hcard : (7 / 8 : ℝ) * #X ^ 2 ≤ #H) (h : #A / (2 * K) ≤ #X) : + #A / (2 ^ 4 * K) ≤ #(oneOfPair H X) := -- by + calc + _ = (#A / (2 * K)) / 8 := by ring + _ ≤ (#X / 8 : ℝ) := by gcongr + _ ≤ #(oneOfPair H X) := + le_of_mul_le_mul_left ((oneOfPair_bound_two hH Hcard).trans_eq' (by ring)) hX lemma quadruple_bound_c {a b : α} {H : Finset (α × α)} (ha : a ∈ oneOfPair H X) (hb : b ∈ oneOfPair H X) (hH : H ⊆ X ×ˢ X) : - (X.card : ℝ) / 2 ≤ (X.filter fun c ↦ (a, c) ∈ H ∧ (b, c) ∈ H).card := by + (#X : ℝ) / 2 ≤ #{c ∈ X | (a, c) ∈ H ∧ (b, c) ∈ H} := by rw [oneOfPair_mem, oneOfPair_mem' hH] at ha hb rw [filter_and, cast_card_inter, ← filter_or] - have : ((X.filter fun c ↦ (a, c) ∈ H ∨ (b, c) ∈ H).card : ℝ) ≤ X.card := by - rw [Nat.cast_le] - exact card_le_card (filter_subset _ _) + have : (#{c ∈ X | (a, c) ∈ H ∨ (b, c) ∈ H} : ℝ) ≤ #X := by gcongr; exact filter_subset .. linarith [ha.2, hb.2, this] variable [AddCommGroup α] lemma quadruple_bound_right {a b : α} (H : Finset (α × α)) (X : Finset α) (h : x = a - b) : - (((X.filter fun c ↦ (a, c) ∈ H ∧ (b, c) ∈ H).sigma fun c ↦ - ((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ - a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c).card : ℝ) ≤ - (((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ - (a₁ - a₂) - (a₃ - a₄) = a - b).card := by + (#({c ∈ X | (a, c) ∈ H ∧ (b, c) ∈ H}.sigma fun c ↦ ((B ×ˢ B) ×ˢ B ×ˢ B).filter + fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c) : ℝ) + ≤ #(((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = a - b) := by rw [← h, Nat.cast_le] refine card_le_card_of_injOn Sigma.snd ?_ ?_ · simp only [not_and, mem_product, and_imp, Prod.forall, mem_sigma, mem_filter, Sigma.forall] @@ -96,12 +90,12 @@ variable {A B : Finset G} {x : G} lemma thing_one : (𝟭_[R] B ○ 𝟭 A) x = ∑ y, 𝟭 A y * 𝟭 B (x + y) := by simp only [dconv_eq_sum_add, conj_indicate_apply, mul_comm] -lemma thing_one_right : (𝟭_[R] A ○ 𝟭 B) x = (A ∩ (x +ᵥ B)).card := by +lemma thing_one_right : (𝟭_[R] A ○ 𝟭 B) x = #(A ∩ (x +ᵥ B)) := by rw [indicate_dconv_indicate_apply] congr 1 apply card_nbij' Prod.fst (fun a ↦ (a, a - x)) <;> aesop (add simp [mem_vadd_finset]) -lemma thing_two : ∑ s, (𝟭_[R] A ○ 𝟭 B) s = A.card * B.card := by +lemma thing_two : ∑ s, (𝟭_[R] A ○ 𝟭 B) s = #A * #B := by simp only [sum_dconv, conj_indicate_apply, sum_indicate] lemma thing_three : ∑ s, ((𝟭 A ○ 𝟭 B) s ^ 2 : R) = E[A, B] := by @@ -113,17 +107,17 @@ lemma thing_three : ∑ s, ((𝟭 A ○ 𝟭 B) s ^ 2 : R) = E[A, B] := by section lemma1 -lemma claim_one : ∑ s, (𝟭_[R] A ○ 𝟭 B) s * (A ∩ (s +ᵥ B)).card = E[A, B] := by +lemma claim_one : ∑ s, (𝟭_[R] A ○ 𝟭 B) s * #(A ∩ (s +ᵥ B)) = E[A, B] := by simp only [← thing_three, ← thing_one_right, sq] lemma claim_two : - (E[A, B]) ^ 2 / (A.card * B.card) ≤ ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (A ∩ (s +ᵥ B)).card ^ 2 := by + (E[A, B]) ^ 2 / (#A * #B) ≤ ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * #(A ∩ (s +ᵥ B)) ^ 2 := by let f := fun s ↦ ((𝟭_[ℝ] A ○ 𝟭 B) s).sqrt have hf : ∀ s, f s ^ 2 = (𝟭_[ℝ] A ○ 𝟭 B) s := by intro s rw [Real.sq_sqrt] exact dconv_nonneg (R := ℝ) indicate_nonneg indicate_nonneg s -- why do I need the annotation?? - have := sum_mul_sq_le_sq_mul_sq univ f (fun s ↦ f s * (A ∩ (s +ᵥ B)).card) + have := sum_mul_sq_le_sq_mul_sq univ f (fun s ↦ f s * #(A ∩ (s +ᵥ B))) refine div_le_of_le_mul₀ (by positivity) ?_ ?_ · refine sum_nonneg fun i _ ↦ ?_ -- indicate nonneg should be a positivity lemma @@ -133,8 +127,8 @@ lemma claim_two : rw [mul_comm] lemma claim_three {H : Finset (G × G)} (hH : H ⊆ A ×ˢ A) : - ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * ((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H).card = - ∑ ab in H, ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (𝟭 B (ab.1 - s) * 𝟭 B (ab.2 - s)) := by + ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * #((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H) = + ∑ ab ∈ H, ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (𝟭 B (ab.1 - s) * 𝟭 B (ab.2 - s)) := by simp only [sum_comm (s := H), ← mul_sum] refine sum_congr rfl fun x _ ↦ ?_ congr 1 @@ -146,9 +140,9 @@ lemma claim_three {H : Finset (G × G)} (hH : H ⊆ A ×ˢ A) : lemma claim_four (ab : G × G) : ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (𝟭 B (ab.1 - s) * 𝟭 B (ab.2 - s)) ≤ - B.card * (𝟭 B ○ 𝟭 B) (ab.1 - ab.2) := by + #B * (𝟭 B ○ 𝟭 B) (ab.1 - ab.2) := by rcases ab with ⟨a, b⟩ - have : ∀ s, (𝟭_[ℝ] A ○ 𝟭 B) s ≤ B.card := fun s ↦ by + have : ∀ s, (𝟭_[ℝ] A ○ 𝟭 B) s ≤ #B := fun s ↦ by simp only [dconv_eq_sum_add, conj_indicate_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one] simp only [indicate_apply, mul_boole, ← sum_filter (· ∈ B), filter_mem_eq_inter, univ_inter] refine sum_le_sum fun i _ ↦ ?_ @@ -156,7 +150,7 @@ lemma claim_four (ab : G × G) : · rfl · exact zero_le_one have : ∑ s : G, (𝟭_[ℝ] A ○ 𝟭 B) s * (𝟭 B ((a, b).1 - s) * 𝟭 B ((a, b).2 - s)) ≤ - B.card * ∑ s : G, (𝟭 B ((a, b).1 - s) * 𝟭 B ((a, b).2 - s)) := by + #B * ∑ s : G, (𝟭 B ((a, b).1 - s) * 𝟭 B ((a, b).2 - s)) := by rw [mul_sum] refine sum_le_sum fun i _ ↦ ?_ exact mul_le_mul_of_nonneg_right (this _) (mul_nonneg (indicate_nonneg _) (indicate_nonneg _)) @@ -166,48 +160,40 @@ lemma claim_four (ab : G × G) : exact Fintype.sum_equiv (Equiv.subLeft b) _ _ $ by simp lemma claim_five {H : Finset (G × G)} (hH : H ⊆ A ×ˢ A) : - ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * ((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H).card ≤ - B.card * ∑ ab in H, (𝟭 B ○ 𝟭 B) (ab.1 - ab.2) := by + ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * #((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H) ≤ + #B * ∑ ab ∈ H, (𝟭 B ○ 𝟭 B) (ab.1 - ab.2) := by rw [claim_three hH, mul_sum] exact sum_le_sum fun ab _ ↦ claim_four ab noncomputable def H_choice (A B : Finset G) (c : ℝ) : Finset (G × G) := - (A ×ˢ A).filter - fun ab ↦ - (𝟭_[ℝ] B ○ 𝟭 B) (ab.1 - ab.2) ≤ c / 2 * (E[A, B] ^ 2 / (A.card ^ 3 * B.card ^ 2)) + {ab ∈ A ×ˢ A | (𝟭_[ℝ] B ○ 𝟭 B) (ab.1 - ab.2) ≤ c / 2 * (E[A, B] ^ 2 / (#A ^ 3 * #B ^ 2))} --- lemma H_choice_subset : lemma claim_six (c : ℝ) (hc : 0 ≤ c) : - ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * ((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c).card ≤ - c / 2 * (E[A, B] ^ 2 / (A.card * B.card)) := by + ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * #((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c) ≤ + c / 2 * (E[A, B] ^ 2 / (#A * #B)) := by refine (claim_five (filter_subset _ _)).trans ?_ - have : ∑ ab in H_choice A B c, (𝟭_[ℝ] B ○ 𝟭 B) (ab.1 - ab.2) ≤ - (H_choice A B c).card * (c / 2 * (E[A, B] ^ 2 / (A.card ^ 3 * B.card ^ 2))) := by + have : ∑ ab ∈ H_choice A B c, (𝟭_[ℝ] B ○ 𝟭 B) (ab.1 - ab.2) ≤ + #(H_choice A B c) * (c / 2 * (E[A, B] ^ 2 / (#A ^ 3 * #B ^ 2))) := by rw [← nsmul_eq_mul] - refine sum_le_card_nsmul _ _ _ ?_ - intro x hx - exact (mem_filter.1 hx).2 - have hA : ((H_choice A B c).card : ℝ) ≤ A.card ^ 2 := by + exact sum_le_card_nsmul _ _ _ fun x hx ↦ (mem_filter.1 hx).2 + have hA : (#(H_choice A B c) : ℝ) ≤ #A ^ 2 := by norm_cast exact (card_le_card (filter_subset _ _)).trans_eq (by simp [sq]) refine (mul_le_mul_of_nonneg_left this (by positivity)).trans ?_ - rcases A.card.eq_zero_or_pos with hA | hA - · rw [hA] - simp - rcases B.card.eq_zero_or_pos with hB | hB - · rw [hB] - simp + obtain rfl | hA := A.eq_empty_or_nonempty + · simp + obtain rfl | hA := B.eq_empty_or_nonempty + · simp calc - _ ≤ (B.card : ℝ) * (A.card ^ 2 * (c / 2 * (E[A, B] ^ 2 / (A.card ^ 3 * B.card ^ 2)))) - := by gcongr - _ = c / 2 * (E[A, B] ^ 2 / (card A * card B)) := by field_simp; ring + _ ≤ (#B : ℝ) * (#A ^ 2 * (c / 2 * (E[A, B] ^ 2 / (#A ^ 3 * #B ^ 2)))) := by gcongr + _ = c / 2 * (E[A, B] ^ 2 / (#A * #B)) := by field_simp; ring -lemma claim_seven (c : ℝ) (hc : 0 ≤ c) (hA : (0 : ℝ) < card A) (hB : (0 : ℝ) < card B) : +lemma claim_seven (c : ℝ) (hc : 0 ≤ c) (hA : (0 : ℝ) < #A) (hB : (0 : ℝ) < #B) : ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * - ((c / 2) * (E[A, B] ^ 2 / (A.card ^ 2 * B.card ^ 2)) + - ((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c).card) ≤ - ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (c * (A ∩ (s +ᵥ B)).card ^ 2) := - calc _ = (c / 2 * (E[A, B] ^ 2 / (card A * card B))) + + ((c / 2) * (E[A, B] ^ 2 / (#A ^ 2 * #B ^ 2)) + + #((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c)) ≤ + ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (c * #(A ∩ (s +ᵥ B)) ^ 2) := + calc _ = (c / 2 * (E[A, B] ^ 2 / (#A * #B))) + ∑ x : G, (𝟭_[ℝ] A ○ 𝟭 B) x * (card ((A ∩ (x +ᵥ B)) ×ˢ (A ∩ (x +ᵥ B)) ∩ H_choice A B c)) := by simp only [mul_add, sum_add_distrib, ← sum_mul, thing_two, ← mul_pow] field_simp @@ -219,10 +205,10 @@ lemma claim_seven (c : ℝ) (hc : 0 ≤ c) (hA : (0 : ℝ) < card A) (hB : (0 : gcongr exact claim_two -lemma claim_eight (c : ℝ) (hc : 0 ≤ c) (hA : (0 : ℝ) < card A) (hB : (0 : ℝ) < card B) : - ∃ s : G, ((c / 2) * (E[A, B] ^ 2 / (A.card ^ 2 * B.card ^ 2)) + - ((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c).card) ≤ - c * (A ∩ (s +ᵥ B)).card ^ 2 := by +lemma claim_eight (c : ℝ) (hc : 0 ≤ c) (hA : (0 : ℝ) < #A) (hB : (0 : ℝ) < #B) : + ∃ s : G, ((c / 2) * (E[A, B] ^ 2 / (#A ^ 2 * #B ^ 2)) + + #((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c)) ≤ + c * #(A ∩ (s +ᵥ B)) ^ 2 := by by_contra! refine (claim_seven c hc hA hB).not_lt ?_ refine sum_lt_sum ?_ ?_ @@ -248,17 +234,15 @@ lemma test_case {E A B : ℕ} {K : ℝ} (hK : 0 < K) (hE : K⁻¹ * (A ^ 2 * B) field_simp ring -lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K) - (hE : K⁻¹ * (A.card ^ 2 * B.card) ≤ E[A, B]) - (hA : (0 : ℝ) < card A) (hB : (0 : ℝ) < card B) : - ∃ s : G, ∃ X ⊆ A ∩ (s +ᵥ B), A.card / (Real.sqrt 2 * K) ≤ X.card ∧ - (1 - c) * X.card ^ 2 ≤ - ((X ×ˢ X).filter - (fun ⟨a, b⟩ ↦ c / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (a - b))).card := by +lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K) (hE : K⁻¹ * (#A ^ 2 * #B) ≤ E[A, B]) + (hA : (0 : ℝ) < #A) (hB : (0 : ℝ) < #B) : + ∃ s : G, ∃ X ⊆ A ∩ (s +ᵥ B), #A / (Real.sqrt 2 * K) ≤ #X ∧ + (1 - c) * #X ^ 2 ≤ + #((X ×ˢ X).filter (fun ⟨a, b⟩ ↦ c / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (a - b))) := by obtain ⟨s, hs⟩ := claim_eight c hc.le hA hB set X := A ∩ (s +ᵥ B) refine ⟨s, X, subset_rfl, ?_, ?_⟩ - · have : (2 : ℝ)⁻¹ * (E[A, B] / (card A * card B)) ^ 2 ≤ (card X) ^ 2 := by + · have : (2 : ℝ)⁻¹ * (E[A, B] / (#A * #B)) ^ 2 ≤ (card X) ^ 2 := by refine le_of_mul_le_mul_left ?_ hc exact ((le_add_of_nonneg_right (Nat.cast_nonneg _)).trans hs).trans_eq' (by ring) replace := Real.sqrt_le_sqrt this @@ -288,18 +272,17 @@ lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K) rw [mul_assoc] gcongr _ * ?_ field_simp [hA, hB, hK, le_div_iff₀, div_le_iff₀] at hE ⊢ - convert_to (A.card ^ 2 * B.card) ^ 2 ≤ (E[A, B] * K) ^ 2 + convert_to (#A ^ 2 * #B) ^ 2 ≤ (E[A, B] * K) ^ 2 · ring_nf · ring_nf gcongr lemma lemma_one' {c K : ℝ} (hc : 0 < c) (hK : 0 < K) - (hE : K⁻¹ * (A.card ^ 2 * B.card) ≤ E[A, B]) - (hA : (0 : ℝ) < card A) (hB : (0 : ℝ) < card B) : - ∃ s : G, ∃ X ⊆ A ∩ (s +ᵥ B), A.card / (2 * K) ≤ X.card ∧ - (1 - c) * X.card ^ 2 ≤ - ((X ×ˢ X).filter - (fun ⟨a, b⟩ ↦ c / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (a - b))).card := by + (hE : K⁻¹ * (#A ^ 2 * #B) ≤ E[A, B]) + (hA : (0 : ℝ) < #A) (hB : (0 : ℝ) < #B) : + ∃ s : G, ∃ X ⊆ A ∩ (s +ᵥ B), #A / (2 * K) ≤ #X ∧ + (1 - c) * #X ^ 2 ≤ + #((X ×ˢ X).filter fun ⟨a, b⟩ ↦ c / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (a - b)) := by obtain ⟨s, X, hX₁, hX₂, hX₃⟩ := lemma_one hc hK hE hA hB refine ⟨s, X, hX₁, hX₂.trans' ?_, hX₃⟩ gcongr _ / (?_ * _) @@ -312,28 +295,27 @@ section lemma2 open Pointwise -lemma many_pairs {K : ℝ} {x : G} - (hab : (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) x) : - A.card / (2 ^ 4 * K ^ 2) ≤ ((B ×ˢ B).filter (fun ⟨c, d⟩ ↦ c - d = x)).card := - calc _ = (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card := by ring - _ ≤ (𝟭 B ○ 𝟭 B) x := hab - _ ≤ ((B ×ˢ B).filter (fun ⟨c, d⟩ ↦ c - d = x)).card := by - rw [indicate_dconv_indicate_apply _ _ _] +lemma many_pairs {K : ℝ} {x : G} (hab : (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) x) : + #A / (2 ^ 4 * K ^ 2) ≤ #((B ×ˢ B).filter fun ⟨c, d⟩ ↦ c - d = x) := + calc + _ = (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A := by ring + _ ≤ (𝟭 B ○ 𝟭 B) x := hab + _ ≤ #((B ×ˢ B).filter fun ⟨c, d⟩ ↦ c - d = x) := by rw [indicate_dconv_indicate_apply] variable {H : Finset (G × G)} {X : Finset G} lemma quadruple_bound_part {K : ℝ} (a c : G) - (hac : (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (a - c)) : - A.card / (2 ^ 4 * K ^ 2) ≤ ((B ×ˢ B).filter fun ⟨a₁, a₂⟩ ↦ a₁ - a₂ = a - c).card := + (hac : (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (a - c)) : + #A / (2 ^ 4 * K ^ 2) ≤ #((B ×ˢ B).filter fun ⟨a₁, a₂⟩ ↦ a₁ - a₂ = a - c) := many_pairs hac lemma quadruple_bound_other {a b c : G} {K : ℝ} {H : Finset (G × G)} (hac : (a, c) ∈ H) (hbc : (b, c) ∈ H) - (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2)) : - (A.card / (2 ^ 4 * K ^ 2)) ^ 2 ≤ (((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ - a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c).card := by - change (_ : ℝ) ≤ (((B ×ˢ B) ×ˢ B ×ˢ B).filter fun (z : (G × G) × G × G) ↦ - z.1.1 - z.1.2 = a - c ∧ z.2.1 - z.2.2 = b - c).card + (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2)) : + (#A / (2 ^ 4 * K ^ 2)) ^ 2 ≤ #(((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ + a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c) := by + change (_ : ℝ) ≤ #(((B ×ˢ B) ×ˢ B ×ˢ B).filter fun (z : (G × G) × G × G) ↦ + z.1.1 - z.1.2 = a - c ∧ z.2.1 - z.2.2 = b - c) rw [filter_product (s := B ×ˢ B) (t := B ×ˢ B) (fun z ↦ z.1 - z.2 = a - c) (fun z ↦ z.1 - z.2 = b - c), card_product, sq, Nat.cast_mul] gcongr ?_ * ?_ @@ -342,29 +324,29 @@ lemma quadruple_bound_other {a b c : G} {K : ℝ} {H : Finset (G × G)} lemma quadruple_bound_left {a b : G} {K : ℝ} {H : Finset (G × G)} (ha : a ∈ oneOfPair H X) (hb : b ∈ oneOfPair H X) - (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2)) + (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2)) (hH' : H ⊆ X ×ˢ X) : - ((X.card : ℝ) / 2) * (A.card / (2 ^ 4 * K ^ 2)) ^ 2 ≤ - ((X.filter fun c ↦ (a, c) ∈ H ∧ (b, c) ∈ H).sigma fun c ↦ + #X / 2 * (#A / (2 ^ 4 * K ^ 2)) ^ 2 ≤ + #({c ∈ X | (a, c) ∈ H ∧ (b, c) ∈ H}.sigma fun c ↦ ((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ - a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c).card := - calc _ ≤ ∑ _x in X.filter fun c ↦ (a, c) ∈ H ∧ (b, c) ∈ H, - ((A.card / (2 ^ 4 * K ^ 2)) ^ 2 : ℝ) := by - rw [sum_const, nsmul_eq_mul] - gcongr ?_ * _ - exact quadruple_bound_c ha hb hH' - _ ≤ ∑ c in X.filter fun c ↦ (a, c) ∈ H ∧ (b, c) ∈ H, - ((((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ((a₁, a₂), a₃, a₄) ↦ - a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c).card : ℝ) := sum_le_sum <| fun i hi ↦ by - simp only [not_and, mem_filter] at hi - exact quadruple_bound_other hi.2.1 hi.2.2 hH - _ = _ := by rw [card_sigma, Nat.cast_sum] + a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c) := + calc + _ ≤ ∑ c ∈ X with (a, c) ∈ H ∧ (b, c) ∈ H, ((#A / (2 ^ 4 * K ^ 2)) ^ 2 : ℝ) := by + rw [sum_const, nsmul_eq_mul] + gcongr ?_ * _ + exact quadruple_bound_c ha hb hH' + _ ≤ ∑ c ∈ X with (a, c) ∈ H ∧ (b, c) ∈ H, (#(((B ×ˢ B) ×ˢ B ×ˢ B).filter + fun ((a₁, a₂), a₃, a₄) ↦ a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c) : ℝ) := by + gcongr with i hi + simp only [not_and, mem_filter] at hi + exact quadruple_bound_other hi.2.1 hi.2.2 hH + _ = _ := by rw [card_sigma, Nat.cast_sum] lemma quadruple_bound {K : ℝ} {x : G} (hx : x ∈ oneOfPair H X - oneOfPair H X) - (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2)) + (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2)) (hH' : H ⊆ X ×ˢ X) : - (A.card ^ 2 * X.card) / (2 ^ 9 * K ^ 4) ≤ - (((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = x).card := by + (#A ^ 2 * #X) / (2 ^ 9 * K ^ 4) ≤ + #(((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = x) := by rw [mem_sub] at hx obtain ⟨a, ha, b, hb, rfl⟩ := hx refine (quadruple_bound_right H X rfl).trans' ?_ @@ -372,38 +354,35 @@ lemma quadruple_bound {K : ℝ} {x : G} (hx : x ∈ oneOfPair H X - oneOfPair H ring lemma big_quadruple_bound {K : ℝ} - (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2)) + (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2)) (hH' : H ⊆ X ×ˢ X) - (hX : A.card / (2 * K) ≤ X.card) : - ((oneOfPair H X - oneOfPair H X).card) * (A.card ^ 3 / (2 ^ 10 * K ^ 5)) ≤ - B.card ^ 4 := - calc _ = ((oneOfPair H X - oneOfPair H X).card) * - ((A.card ^ 2 * (A.card / (2 * K))) / (2 ^ 9 * K ^ 4)) := by ring - _ ≤ ((oneOfPair H X - oneOfPair H X).card) * - ((A.card ^ 2 * X.card) / (2 ^ 9 * K ^ 4)) := by gcongr - _ = ∑ _x in oneOfPair H X - oneOfPair H X, - ((A.card ^ 2 * X.card) / (2 ^ 9 * K ^ 4) : ℝ) := by simp - _ ≤ ∑ x in oneOfPair H X - oneOfPair H X, - ((((B ×ˢ B) ×ˢ B ×ˢ B).filter - fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = x).card : ℝ) := - sum_le_sum fun x hx ↦ quadruple_bound hx hH hH' - _ ≤ ∑ x, ((((B ×ˢ B) ×ˢ B ×ˢ B).filter - fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = x).card : ℝ) := - sum_le_sum_of_subset_of_nonneg (subset_univ _) (fun _ _ _ ↦ by positivity) - _ = _ := by - rw [← Nat.cast_sum, ← card_eq_sum_card_fiberwise] - · simp only [card_product, Nat.cast_mul] - ring_nf - · simp - -theorem BSG_aux {K : ℝ} (hK : 0 < K) (hA : (0 : ℝ) < A.card) (hB : (0 : ℝ) < B.card) - (hAB : K⁻¹ * (A.card ^ 2 * B.card) ≤ E[A, B]) : - ∃ s : G, ∃ A' ⊆ A ∩ (s +ᵥ B), (2 ^ 4 : ℝ)⁻¹ * K⁻¹ * A.card ≤ A'.card ∧ - (A' - A').card ≤ 2 ^ 10 * K ^ 5 * B.card ^ 4 / A.card ^ 3 := by + (hX : #A / (2 * K) ≤ #X) : + (#(oneOfPair H X - oneOfPair H X)) * (#A ^ 3 / (2 ^ 10 * K ^ 5)) ≤ #B ^ 4 := + calc + _ = (#(oneOfPair H X - oneOfPair H X)) * ((#A ^ 2 * (#A / (2 * K))) / (2 ^ 9 * K ^ 4)) := by + ring + _ ≤ (#(oneOfPair H X - oneOfPair H X)) * ((#A ^ 2 * #X) / (2 ^ 9 * K ^ 4)) := by gcongr + _ = ∑ _x ∈ oneOfPair H X - oneOfPair H X, ((#A ^ 2 * #X) / (2 ^ 9 * K ^ 4) : ℝ) := by simp + _ ≤ ∑ x ∈ oneOfPair H X - oneOfPair H X, + (#(((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = x) : ℝ) := + sum_le_sum fun x hx ↦ quadruple_bound hx hH hH' + _ ≤ ∑ x, (#(((B ×ˢ B) ×ˢ B ×ˢ B).filter + fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = x) : ℝ) := by + gcongr; exact subset_univ _ + _ = _ := by + rw [← Nat.cast_sum, ← card_eq_sum_card_fiberwise] + · simp only [card_product, Nat.cast_mul] + ring_nf + · simp + +theorem BSG_aux {K : ℝ} (hK : 0 < K) (hA : (0 : ℝ) < #A) (hB : (0 : ℝ) < #B) + (hAB : K⁻¹ * (#A ^ 2 * #B) ≤ E[A, B]) : + ∃ s : G, ∃ A' ⊆ A ∩ (s +ᵥ B), (2 ^ 4)⁻¹ * K⁻¹ * #A ≤ #A' ∧ + #(A' - A') ≤ 2 ^ 10 * K ^ 5 * #B ^ 4 / #A ^ 3 := by obtain ⟨s, X, hX₁, hX₂, hX₃⟩ := lemma_one' (c := 1 / 8) (by norm_num) hK hAB hA hB set H : Finset (G × G) := (X ×ˢ X).filter - fun ⟨a, b⟩ ↦ (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (a - b) - have : (0 : ℝ) < X.card := hX₂.trans_lt' (by positivity) + fun ⟨a, b⟩ ↦ (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (a - b) + have : (0 : ℝ) < #X := hX₂.trans_lt' (by positivity) refine ⟨s, oneOfPair H X, (filter_subset _ _).trans hX₁, ?_, ?_⟩ · rw [← mul_inv, inv_mul_eq_div] exact oneOfPair_bound (filter_subset _ _) this (hX₃.trans_eq' (by norm_num)) hX₂ @@ -412,9 +391,8 @@ theorem BSG_aux {K : ℝ} (hK : 0 < K) (hA : (0 : ℝ) < A.card) (hB : (0 : ℝ) rw [mul_div_assoc', div_le_iff₀ (by positivity)] at this exact this.trans_eq (by ring) -theorem BSG {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (A.card ^ 2 * B.card) ≤ E[A, B]) : - ∃ A' ⊆ A, (2 ^ 4 : ℝ)⁻¹ * K⁻¹ * A.card ≤ A'.card ∧ - (A' - A').card ≤ 2 ^ 10 * K ^ 5 * B.card ^ 4 / A.card ^ 3 := by +theorem BSG {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (#A ^ 2 * #B) ≤ E[A, B]) : + ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * #A ≤ #A' ∧ #(A' - A') ≤ 2 ^ 10 * K ^ 5 * #B ^ 4 / #A ^ 3 := by obtain rfl | hA := A.eq_empty_or_nonempty · exact ⟨∅, by simp⟩ obtain rfl | hK := eq_or_lt_of_le hK @@ -422,10 +400,9 @@ theorem BSG {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (A.card ^ · obtain ⟨s, A', hA, h⟩ := BSG_aux hK (by simpa [card_pos]) (by simpa [card_pos]) hAB exact ⟨A', hA.trans (inter_subset_left ..), h⟩ -theorem BSG₂ {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (A.card ^ 2 * B.card) ≤ E[A, B]) : - ∃ A' ⊆ A, ∃ B' ⊆ B, (2 ^ 4 : ℝ)⁻¹ * K⁻¹ * A.card ≤ A'.card ∧ - (2 ^ 4 : ℝ)⁻¹ * K⁻¹ * A.card ≤ B'.card ∧ - (A' - B').card ≤ 2 ^ 10 * K ^ 5 * B.card ^ 4 / A.card ^ 3 := by +theorem BSG₂ {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (#A ^ 2 * #B) ≤ E[A, B]) : + ∃ A' ⊆ A, ∃ B' ⊆ B, (2 ^ 4)⁻¹ * K⁻¹ * #A ≤ #A' ∧ + (2 ^ 4)⁻¹ * K⁻¹ * #A ≤ #B' ∧ #(A' - B') ≤ 2 ^ 10 * K ^ 5 * #B ^ 4 / #A ^ 3 := by obtain rfl | hA := A.eq_empty_or_nonempty · exact ⟨∅, by simp, ∅, by simp⟩ obtain rfl | hK := eq_or_lt_of_le hK @@ -442,9 +419,8 @@ theorem BSG₂ {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (A.car rw [add_vadd_comm] apply card_vadd_finset -theorem BSG_self {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * A.card ^ 3 ≤ E[A]) : - ∃ A' ⊆ A, (2 ^ 4 : ℝ)⁻¹ * K⁻¹ * A.card ≤ A'.card ∧ - (A' - A').card ≤ 2 ^ 10 * K ^ 5 * A.card := by +theorem BSG_self {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * #A ^ 3 ≤ E[A]) : + ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * #A ≤ #A' ∧ #(A' - A') ≤ 2 ^ 10 * K ^ 5 * #A := by convert BSG hK hA ?_ using 5 · have := hA.card_pos field_simp @@ -452,13 +428,12 @@ theorem BSG_self {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * A.ca · ring_nf assumption -theorem BSG_self' {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * A.card ^ 3 ≤ E[A]) : - ∃ A' ⊆ A, (2 ^ 4 : ℝ)⁻¹ * K⁻¹ * A.card ≤ A'.card ∧ - (A' - A').card ≤ 2 ^ 14 * K ^ 6 * A'.card := by +theorem BSG_self' {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * #A ^ 3 ≤ E[A]) : + ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * #A ≤ #A' ∧ #(A' - A') ≤ 2 ^ 14 * K ^ 6 * #A' := by obtain ⟨A', hA', hAA', hAK'⟩ := BSG_self hK hA hAK refine ⟨A', hA', hAA', hAK'.trans ?_⟩ calc - _ = 2 ^ 14 * K ^ 6 * ((2 ^ 4)⁻¹ * K⁻¹ * A.card) := ?_ + _ = 2 ^ 14 * K ^ 6 * ((2 ^ 4)⁻¹ * K⁻¹ * #A) := ?_ _ ≤ _ := by gcongr obtain rfl | hK := hK.eq_or_lt · simp diff --git a/LeanAPAP/FiniteField.lean b/LeanAPAP/FiniteField.lean index 7de83ce29c..c38d97bfa7 100644 --- a/LeanAPAP/FiniteField.lean +++ b/LeanAPAP/FiniteField.lean @@ -158,7 +158,7 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε _ ≤ 1 := by linarith obtain ⟨T, hTcard, hTε⟩ := AlmostPeriodicity.linfty_almost_periodicity_boosted ε hε₀ hε₁ k (by positivity) (le_inv_of_le_inv₀ (by positivity) hα₂) hA₁ univ_nonempty S A₂ hS hA₂ - have hT : 0 < (T.card : ℝ) := hTcard.trans_lt' (by positivity) + have hT : 0 < (#T : ℝ) := hTcard.trans_lt' (by positivity) replace hT : T.Nonempty := by simpa using hT let Δ := largeSpec (μ T) 2⁻¹ let V : Submodule (ZMod q) G := AddSubgroup.toZModSubmodule _ $ ⨅ γ ∈ Δ, γ.toAddMonoidHom.ker @@ -170,9 +170,9 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε have hWV : W ≤ V := by sorry have := calc - log T.dens⁻¹ ≤ log (α⁻¹ ^ (-4096 * ⌈𝓛 (min 1 (A₂.card / S.card))⌉ * k ^ 2 / ε ^ 2))⁻¹ := by + log T.dens⁻¹ ≤ log (α⁻¹ ^ (-4096 * ⌈𝓛 (min 1 (#A₂ / #S))⌉ * k ^ 2 / ε ^ 2))⁻¹ := by gcongr; rwa [nnratCast_dens, le_div_iff₀]; positivity - _ = 2 ^ 12 * log α⁻¹ * ⌈𝓛 (min 1 (A₂.card / S.card))⌉ * k ^ 2 / ε ^ 2 := by + _ = 2 ^ 12 * log α⁻¹ * ⌈𝓛 (min 1 (#A₂ / #S))⌉ * k ^ 2 / ε ^ 2 := by rw [log_inv, log_rpow (by positivity)]; ring_nf _ ≤ 2 ^ 12 * log α⁻¹ * ⌈𝓛 (min 1 A₂.dens)⌉ * k ^ 2 / ε ^ 2 := by rw [nnratCast_dens, ← card_univ]; gcongr; exact S.subset_univ @@ -194,7 +194,7 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε (↑(finrank (ZMod q) G - finrank (ZMod q) V) : ℝ) ≤ ↑(finrank (ZMod q) G - finrank (ZMod q) W) := by gcongr; exact Submodule.finrank_mono hWV - _ ≤ Δ'.card := sorry + _ ≤ #Δ' := sorry _ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖μ T‖_[1] ^ 2 / ‖μ T‖_[2] ^ 2 / card G)⌉₊ / 2⁻¹ ^ 2⌉₊ := by gcongr _ = ⌈2 ^ 7 * exp 1 ^ 2 * ⌈𝓛 T.dens⌉₊⌉₊ := by diff --git a/LeanAPAP/Integer.lean b/LeanAPAP/Integer.lean index 65123147ef..41af146e92 100644 --- a/LeanAPAP/Integer.lean +++ b/LeanAPAP/Integer.lean @@ -4,4 +4,4 @@ import Mathlib.Combinatorics.Additive.AP.Three.Defs open Finset Real theorem int {A : Finset ℕ} {N : ℕ} (hAN : A ⊆ range N) (hA : ThreeAPFree (α := ℕ) A) : - ∃ c > 0, A.card ≤ N / exp (- c * log N ^ (12⁻¹ : ℝ)) := sorry + ∃ c > 0, #A ≤ N / exp (- c * log N ^ (12⁻¹ : ℝ)) := sorry diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index 8aac4a5e15..9f010181f7 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -20,8 +20,8 @@ section Add variable [Add α] lemma big_shifts_step1 (L : Finset (Fin k → α)) (hk : k ≠ 0) : - ∑ x in L + s.piDiag (Fin k), ∑ l in L, ∑ s in s.piDiag (Fin k), (if l + s = x then 1 else 0) - = L.card * s.card := by + ∑ x ∈ L + s.piDiag (Fin k), ∑ l ∈ L, ∑ s ∈ s.piDiag (Fin k), (if l + s = x then 1 else 0) + = #L * #s := by simp only [@sum_comm _ _ _ _ (L + _), sum_ite_eq] rw [sum_const_nat] intro l hl @@ -34,10 +34,9 @@ end Add variable [AddCommGroup α] [Fintype α] lemma reindex_count (L : Finset (Fin k → α)) (hk : k ≠ 0) (hL' : L.Nonempty) (l₁ : Fin k → α) : - ∑ l₂ in L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 = - (univ.filter fun t ↦ (l₁ - fun _ ↦ t) ∈ L).card := + ∑ l₂ ∈ L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 = #{t | (l₁ - fun _ ↦ t) ∈ L} := calc - _ = ∑ l₂ in L, ∑ t : α, ite ((l₁ - fun _ ↦ t) = l₂) 1 0 := by + _ = ∑ l₂ ∈ L, ∑ t : α, ite ((l₁ - fun _ ↦ t) = l₂) 1 0 := by refine sum_congr rfl fun l₂ hl₂ ↦ ?_ rw [Fintype.sum_ite_eq_ite_exists] simp only [mem_piDiag, mem_univ, eq_sub_iff_add_eq, true_and, sub_eq_iff_eq_add', @@ -47,7 +46,7 @@ lemma reindex_count (L : Finset (Fin k → α)) (hk : k ≠ 0) (hL' : L.Nonempty cases k · simp at hk · simpa using congr_fun h 0 - _ = (univ.filter fun t ↦ (l₁ - fun _ ↦ t) ∈ L).card := by + _ = #{t | (l₁ - fun _ ↦ t) ∈ L} := by simp only [sum_comm, sum_ite_eq, card_eq_sum_ones, sum_filter] end Finset @@ -56,8 +55,8 @@ section variable {α : Type*} {g : α → ℝ} {c ε : ℝ} {A : Finset α} open Finset -lemma my_markov (hc : 0 < c) (hg : ∀ a ∈ A, 0 ≤ g a) (h : ∑ a in A, g a ≤ ε * c * A.card) : - (1 - ε) * A.card ≤ (A.filter (g · ≤ c)).card := by +lemma my_markov (hc : 0 < c) (hg : ∀ a ∈ A, 0 ≤ g a) (h : ∑ a ∈ A, g a ≤ ε * c * #A) : + (1 - ε) * #A ≤ #{a ∈ A | g a ≤ c} := by classical have := h.trans' (sum_le_sum_of_subset_of_nonneg (filter_subset (¬g · ≤ c) A) fun i hi _ ↦ hg _ hi) @@ -69,7 +68,7 @@ lemma my_markov (hc : 0 < c) (hg : ∀ a ∈ A, 0 ≤ g a) (h : ∑ a in A, g a linarith only [this] lemma my_other_markov (hc : 0 ≤ c) (hε : 0 ≤ ε) (hg : ∀ a ∈ A, 0 ≤ g a) - (h : ∑ a in A, g a ≤ ε * c * A.card) : (1 - ε) * A.card ≤ (A.filter (g · ≤ c)).card := by + (h : ∑ a ∈ A, g a ≤ ε * c * #A) : (1 - ε) * #A ≤ #{a ∈ A | g a ≤ c} := by rcases hc.lt_or_eq with (hc | rfl) · exact my_markov hc hg h simp only [mul_zero, zero_mul] at h @@ -98,16 +97,16 @@ section variable [MeasurableSpace G] [DiscreteMeasurableSpace G] lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hk : 64 * m / ε ^ 2 ≤ k) : - (8 * m) ^ m * k ^ (m - 1) * A.card ^ k * k * (2 * ‖f‖_[2 * m] : ℝ) ^ (2 * m) ≤ - 1 / 2 * ((k * ε) ^ (2 * m) * ∑ i : G, ‖f i‖ ^ (2 * m)) * ↑A.card ^ k := by + (8 * m) ^ m * k ^ (m - 1) * #A ^ k * k * (2 * ‖f‖_[2 * m] : ℝ) ^ (2 * m) ≤ + 1 / 2 * ((k * ε) ^ (2 * m) * ∑ i : G, ‖f i‖ ^ (2 * m)) * #A ^ k := by have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two] have hm' : 2 * m ≠ 0 := by refine mul_ne_zero two_pos.ne' ?_ rw [← pos_iff_ne_zero, ← Nat.succ_le_iff] exact hm rw [mul_pow (2 : ℝ), ← hmeq, ← dLpNorm_pow_eq_sum_norm hm' f, ← mul_assoc, ← mul_assoc, - mul_right_comm _ (A.card ^ k : ℝ), mul_right_comm _ (A.card ^ k : ℝ), - mul_right_comm _ (A.card ^ k : ℝ)] + mul_right_comm _ (#A ^ k : ℝ), mul_right_comm _ (#A ^ k : ℝ), + mul_right_comm _ (#A ^ k : ℝ)] gcongr ?_ * _ * _ rw [mul_assoc (_ ^ m : ℝ), ← pow_succ, Nat.sub_add_cancel hm, pow_mul, pow_mul, ← mul_pow, ← mul_pow] @@ -132,9 +131,9 @@ variable [DecidableEq G] [AddCommGroup G] local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s lemma lemma28_part_one (hm : 1 ≤ m) (x : G) : - ∑ a in A ^^ k, ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤ + ∑ a ∈ A ^^ k, ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤ (8 * m) ^ m * k ^ (m - 1) * - ∑ a in A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) := by + ∑ a ∈ A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) := by let f' : G → ℂ := fun a ↦ f (x - a) - (mu A ∗ f) x refine (RCLike.marcinkiewicz_zygmund (by linarith only [hm]) f' ?_).trans_eq' ?_ · intro i @@ -147,22 +146,22 @@ lemma lemma28_part_one (hm : 1 ≤ m) (x : G) : simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin] lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) : - (∑ x in L + S.piDiag (Fin k), ∑ l in L, ∑ s in S.piDiag (Fin k), ite (l + s = x) (1 : ℝ) 0) ^ 2 - ≤ (L + S.piDiag (Fin k)).card * S.card * - ∑ l₁ in L, ∑ l₂ in L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 := by + (∑ x ∈ L + S.piDiag (Fin k), ∑ l ∈ L, ∑ s ∈ S.piDiag (Fin k), ite (l + s = x) (1 : ℝ) 0) ^ 2 + ≤ #(L + S.piDiag (Fin k)) * #S * + ∑ l₁ ∈ L, ∑ l₂ ∈ L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 := by refine sq_sum_le_card_mul_sum_sq.trans ?_ simp_rw [sq, sum_mul, @sum_comm _ _ _ _ (L + S.piDiag (Fin k)), boole_mul, sum_ite_eq, mul_assoc] refine mul_le_mul_of_nonneg_left ?_ (Nat.cast_nonneg _) have : ∀ f : (Fin k → G) → (Fin k → G) → ℝ, - ∑ x in L, ∑ y in S.piDiag (Fin k), (if x + y ∈ L + S.piDiag (Fin k) then f x y else 0) = - ∑ x in L, ∑ y in S.piDiag (Fin k), f x y := by + ∑ x ∈ L, ∑ y ∈ S.piDiag (Fin k), (if x + y ∈ L + S.piDiag (Fin k) then f x y else 0) = + ∑ x ∈ L, ∑ y ∈ S.piDiag (Fin k), f x y := by refine fun f ↦ sum_congr rfl fun x hx ↦ ?_ exact sum_congr rfl fun y hy ↦ if_pos $ add_mem_add hx hy rw [this] have (x y) : - ∑ s₁ in S.piDiag (Fin k), ∑ s₂ in S.piDiag (Fin k), ite (y + s₂ = x + s₁) (1 : ℝ) 0 = + ∑ s₁ ∈ S.piDiag (Fin k), ∑ s₂ ∈ S.piDiag (Fin k), ite (y + s₂ = x + s₁) (1 : ℝ) 0 = ite (x - y ∈ univ.piDiag (Fin k)) 1 0 * - ∑ s₁ in S.piDiag (Fin k), ∑ s₂ in S.piDiag (Fin k), ite (s₂ = x + s₁ - y) 1 0 := by + ∑ s₁ ∈ S.piDiag (Fin k), ∑ s₂ ∈ S.piDiag (Fin k), ite (s₂ = x + s₁ - y) 1 0 := by simp_rw [mul_sum, boole_mul, ← ite_and] refine sum_congr rfl fun s₁ hs₁ ↦ ?_ refine sum_congr rfl fun s₂ hs₂ ↦ ?_ @@ -176,10 +175,10 @@ lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) : obtain ⟨j, -, rfl⟩ := hs₂ exact mem_image.2 ⟨j - i, mem_univ _, rfl⟩ simp_rw [@sum_comm _ _ _ _ (S.piDiag (Fin k)) L, this, sum_ite_eq'] - have : ∑ x in L, ∑ y in L, + have : ∑ x ∈ L, ∑ y ∈ L, ite (x - y ∈ univ.piDiag (Fin k)) (1 : ℝ) 0 * - ∑ z in S.piDiag (Fin k), ite (x + z - y ∈ S.piDiag (Fin k)) 1 0 ≤ - ∑ x in L, ∑ y in L, ite (x - y ∈ univ.piDiag (Fin k)) 1 0 * (S.card : ℝ) := by + ∑ z ∈ S.piDiag (Fin k), ite (x + z - y ∈ S.piDiag (Fin k)) 1 0 ≤ + ∑ x ∈ L, ∑ y ∈ L, ite (x - y ∈ univ.piDiag (Fin k)) 1 0 * (#S : ℝ) := by refine sum_le_sum fun l₁ _ ↦ sum_le_sum fun l₂ _ ↦ ?_ refine mul_le_mul_of_nonneg_left ?_ (by split_ifs <;> norm_num) refine (sum_le_card_nsmul _ _ 1 ?_).trans_eq ?_ @@ -196,11 +195,11 @@ lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) : lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0) (hL' : L.Nonempty) (hL : L ⊆ A ^^ k) : ∃ a : Fin k → G, a ∈ L ∧ - L.card * S.card ≤ (A + S).card ^ k * (univ.filter fun t : G ↦ (a - fun _ ↦ t) ∈ L).card := by + #L * #S ≤ #(A + S) ^ k * #{t | (a - fun _ ↦ t) ∈ L} := by rcases S.eq_empty_or_nonempty with (rfl | hS) · simpa only [card_empty, mul_zero, zero_le', and_true] using hL' - have hS' : 0 < S.card := by rwa [card_pos] - have : (L + S.piDiag (Fin k)).card ≤ (A + S).card ^ k := by + have hS' : 0 < #S := by rwa [card_pos] + have : #(L + S.piDiag _) ≤ #(A + S) ^ k := by refine (card_le_card (add_subset_add_right hL)).trans ?_ rw [← Fintype.card_piFinset_const] refine card_le_card fun i hi ↦ ?_ @@ -209,13 +208,11 @@ lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0) obtain ⟨y, hy, a, ha, rfl⟩ := hi intro j exact ⟨y j, hy _, a, ha, rfl⟩ - rsuffices ⟨a, ha, h⟩ : ∃ a ∈ L, - L.card * S.card ≤ (L + S.piDiag (Fin k)).card * (univ.filter fun t ↦ (a - fun _ ↦ t) ∈ L).card + rsuffices ⟨a, ha, h⟩ : ∃ a ∈ L, #L * #S ≤ #(L + S.piDiag _) * #{t | (a - fun _ ↦ t) ∈ L} · exact ⟨a, ha, h.trans (Nat.mul_le_mul_right _ this)⟩ clear! A - have : L.card ^ 2 * S.card ≤ - (L + S.piDiag (Fin k)).card * - ∑ l₁ in L, ∑ l₂ in L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 := by + have : #L ^ 2 * #S ≤ + #(L + S.piDiag _) * ∑ l₁ ∈ L, ∑ l₂ ∈ L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 := by refine Nat.le_of_mul_le_mul_left ?_ hS' rw [mul_comm, mul_assoc, ← sq, ← mul_pow, mul_left_comm, ← mul_assoc, ← big_shifts_step1 L hk] exact_mod_cast @big_shifts_step2 G _ _ _ _ _ L hk @@ -235,13 +232,13 @@ def LProp (k m : ℕ) (ε : ℝ) (f : G → ℂ) (A : Finset G) (a : Fin k → G noncomputable instance : DecidablePred (LProp k m ε f A) := Classical.decPred _ noncomputable def l (k m : ℕ) (ε : ℝ) (f : G → ℂ) (A : Finset G) : Finset (Fin k → G) := - (A ^^ k).filter (LProp k m ε f A) + {x ∈ A ^^ k | LProp k m ε f A x} lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m) - (h : ∑ a in A ^^ k, + (h : ∑ a ∈ A ^^ k, (‖fun x : G ↦ ∑ i : Fin k, f (x - a i) - (k • (mu A ∗ f)) x‖_[2 * m] ^ (2 * m) : ℝ) ≤ - 1 / 2 * (k * ε * ‖f‖_[2 * m]) ^ (2 * m) * A.card ^ k) : - (A.card ^ k : ℝ) / 2 ≤ (l k m ε f A).card := by + 1 / 2 * (k * ε * ‖f‖_[2 * m]) ^ (2 * m) * #A ^ k) : + (#A ^ k : ℝ) / 2 ≤ #(l k m ε f A) := by rw [← Nat.cast_pow, ← Fintype.card_piFinset_const] at h have := my_other_markov (by positivity) (by norm_num) (fun _ _ ↦ by positivity) h norm_num1 at this @@ -254,8 +251,8 @@ lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m) variable [DiscreteMeasurableSpace G] lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) : - (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤ - (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := by + (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 -- 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 @@ -273,7 +270,7 @@ lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) : rw [dL1Norm_mu hA, mul_one] lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) : - (A.card ^ k : ℝ) / 2 ≤ (l k m ε f A).card := by + (#A ^ k : ℝ) / 2 ≤ #(l k m ε f A) := by have : 0 < k := by rw [← @Nat.cast_pos ℝ] refine hk.trans_lt' ?_ @@ -288,10 +285,10 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) rw [← hmeq, mul_pow] simp only [dLpNorm_pow_eq_sum_norm hm'] rw [sum_comm] - have : ∀ x : G, ∑ a in A ^^ k, + have : ∀ x : G, ∑ a ∈ A ^^ k, ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤ (8 * m) ^ m * k ^ (m - 1) * - ∑ a in A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) := + ∑ a ∈ A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) := lemma28_part_one hm refine (sum_le_sum fun x _ ↦ this x).trans ?_ rw [← mul_sum] @@ -302,8 +299,8 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) simp only [Pi.sub_apply, translate_apply] simp only [this] have : - (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤ - (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i, (2 * ‖f‖_[2 * m]) ^ (2 * m) := + (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, (2 * ‖f‖_[2 * m]) ^ (2 * m) := lemma28_part_two hm hA refine le_trans (mod_cast this) ?_ simp only [sum_const, Fintype.card_piFinset_const, nsmul_eq_mul, Nat.cast_pow] @@ -391,7 +388,7 @@ lemma T_bound (hK₂ : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ) lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (f : G → ℂ) (hK₂ : 2 ≤ K) (hK : σ[A, S] ≤ K) : ∃ T : Finset G, - K ^ (-512 * m / ε ^ 2 : ℝ) * S.card ≤ T.card ∧ + K ^ (-512 * m / ε ^ 2 : ℝ) * #S ≤ #T ∧ ∀ t ∈ T, ‖τ t (mu A ∗ f) - mu A ∗ f‖_[2 * m] ≤ ε * ‖f‖_[2 * m] := by obtain rfl | hm := m.eq_zero_or_pos · exact ⟨S, by simp⟩ @@ -409,14 +406,14 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) ( let k := ⌈(64 : ℝ) * m / (ε / 2) ^ 2⌉₊ have hk : k ≠ 0 := by positivity let L := l k m (ε / 2) f A - have : (A.card : ℝ) ^ k / 2 ≤ L.card := lemma28 (half_pos hε) hm (Nat.le_ceil _) + have : (#A : ℝ) ^ k / 2 ≤ #L := lemma28 (half_pos hε) hm (Nat.le_ceil _) have hL : L.Nonempty := by rw [← card_pos, ← @Nat.cast_pos ℝ] exact this.trans_lt' (by positivity) obtain ⟨a, ha, hL'⟩ := big_shifts S _ hk hL (filter_subset _ _) - refine ⟨univ.filter fun t : G ↦ (a + fun _ ↦ -t) ∈ L, ?_, ?_⟩ + refine ⟨({t | (a + fun _ ↦ -t) ∈ L} : Finset _), ?_, ?_⟩ · simp_rw [sub_eq_add_neg] at hL' - exact T_bound hK₂ L.card S.card A.card (A + S).card _ rfl hL' this + exact T_bound hK₂ #L #S #A #(A + S) _ rfl hL' this (by rw [← cast_addConst_mul_card]; gcongr) hA.card_pos hε hε' hm intro t ht simp only [exists_prop, exists_eq_right, mem_filter, mem_univ, true_and] at ht @@ -426,10 +423,10 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) ( theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hK₂ : 2 ≤ K) (hK : σ[A, S] ≤ K) (B C : Finset G) (hB : B.Nonempty) (hC : C.Nonempty) : ∃ T : Finset G, - K ^ (-4096 * ⌈𝓛 (C.card / B.card)⌉ / ε ^ 2) * S.card ≤ T.card ∧ + K ^ (-4096 * ⌈𝓛 (#C / #B)⌉ / ε ^ 2) * #S ≤ #T ∧ ∀ t ∈ T, ‖τ t (μ_[ℂ] A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C‖_[∞] ≤ ε := by - let r : ℝ := min 1 (C.card / B.card) - set m : ℝ := 𝓛 (C.card / B.card) + let r : ℝ := min 1 (#C / #B) + set m : ℝ := 𝓛 (#C / #B) have hm₀ : 0 < m := curlog_pos (by positivity) have hm₁ : 1 ≤ ⌈m⌉₊ := Nat.one_le_iff_ne_zero.2 $ by positivity obtain ⟨T, hKT, hT⟩ := almost_periodicity (ε / exp 1) (by positivity) @@ -441,9 +438,9 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ have hM : (M : ℝ≥0).IsConjExponent _ := .conjExponent hM₁ refine ⟨T, ?_, fun t ht ↦ ?_⟩ · calc - _ = K ^(-(512 * 8) / ε ^ 2 * ⌈m⌉₊) * S.card := by + _ = K ^(-(512 * 8) / ε ^ 2 * ⌈m⌉₊) * #S := by rw [mul_div_right_comm, natCast_ceil_eq_intCast_ceil hm₀.le]; norm_num - _ ≤ K ^(-(512 * exp 1 ^ 2) / ε ^ 2 * ⌈m⌉₊) * S.card := by + _ ≤ K ^(-(512 * exp 1 ^ 2) / ε ^ 2 * ⌈m⌉₊) * #S := by gcongr · exact one_le_two.trans hK₂ calc @@ -466,10 +463,10 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ _ ≤ ∑ y, ‖F y * μ (x +ᵥ -C) y‖ := norm_sum_le _ _ _ = ‖F * μ (x +ᵥ -C)‖_[1] := by rw [dL1Norm_eq_sum_norm]; rfl _ ≤ ‖F‖_[M] * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := dL1Norm_mul_le hM _ _ - _ ≤ ε / exp 1 * B.card ^ (M : ℝ)⁻¹ * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := by + _ ≤ ε / exp 1 * #B ^ (M : ℝ)⁻¹ * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := by gcongr simpa only [← ENNReal.coe_natCast, dLpNorm_indicate hM₀] using hT _ ht - _ = ε * ((C.card / B.card) ^ (-(M : ℝ)⁻¹) / exp 1) := by + _ = ε * ((#C / #B) ^ (-(M : ℝ)⁻¹) / exp 1) := by rw [← mul_comm_div, dLpNorm_mu hM.symm.one_le hC.neg.vadd_finset, card_vadd_finset, card_neg, hM.symm.coe.inv_sub_one, div_rpow, mul_assoc, NNReal.coe_natCast] push_cast @@ -477,7 +474,7 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ all_goals positivity _ ≤ ε := mul_le_of_le_one_right (by positivity) $ (div_le_one $ by positivity).2 ?_ calc - (C.card / B.card : ℝ) ^ (-(M : ℝ)⁻¹) + (#C / #B : ℝ) ^ (-(M : ℝ)⁻¹) ≤ r ^ (-(M : ℝ)⁻¹) := rpow_le_rpow_of_nonpos (by positivity) inf_le_right $ neg_nonpos.2 $ by positivity _ ≤ r ^ (-(1 + log r⁻¹)⁻¹) := @@ -496,7 +493,7 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : (hK₂ : 2 ≤ K) (hK : σ[A, S] ≤ K) (hS : S.Nonempty) (B C : Finset G) (hB : B.Nonempty) (hC : C.Nonempty) : ∃ T : Finset G, - K ^ (-4096 * ⌈𝓛 (C.card / B.card)⌉ * k ^ 2/ ε ^ 2) * S.card ≤ T.card ∧ + K ^ (-4096 * ⌈𝓛 (#C / #B)⌉ * k ^ 2/ ε ^ 2) * #S ≤ #T ∧ ‖μ T ∗^ k ∗ (μ_[ℂ] A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C‖_[∞] ≤ ε := by obtain ⟨T, hKT, hT⟩ := linfty_almost_periodicity (ε / k) (by positivity) (div_le_one_of_le₀ (hε₁.trans $ mod_cast Nat.one_le_iff_ne_zero.2 hk) $ by positivity) hK₂ hK @@ -504,7 +501,7 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : refine ⟨T, by simpa only [div_pow, div_div_eq_mul_div] using hKT, ?_⟩ set F := μ_[ℂ] A ∗ 𝟭 B ∗ μ C have hT' : T.Nonempty := by - have : (0 : ℝ) < T.card := hKT.trans_lt' $ by positivity + have : (0 : ℝ) < #T := hKT.trans_lt' $ by positivity simpa [card_pos] using this calc (‖μ T ∗^ k ∗ F - F‖_[∞] : ℝ) diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index b03234478a..14137d6101 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/LeanAPAP/Physics/DRC.lean @@ -20,7 +20,7 @@ private def c (p : ℕ) (A : Finset G) (s : Fin p → G) : Finset G := univ.inf private lemma lemma_0 (p : ℕ) (B₁ B₂ A : Finset G) (f : G → ℝ) : ∑ s, ⟪𝟭_[ℝ] (B₁ ∩ c p A s) ○ 𝟭 (B₂ ∩ c p A s), f⟫_[ℝ] = - (B₁.card * B₂.card) • ∑ x, (μ_[ℝ] B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x := by + (#B₁ * #B₂) • ∑ x, (μ_[ℝ] B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x := by simp_rw [mul_assoc] simp only [wInner_one_eq_sum, inner_apply, RCLike.conj_to_real, mul_sum, sum_mul, smul_sum, @sum_comm _ _ (Fin p → G), sum_dconv_mul, dconv_apply_sub, Fintype.sum_pow, map_indicate] @@ -31,20 +31,20 @@ private lemma lemma_0 (p : ℕ) (B₁ B₂ A : Finset G) (f : G → ℝ) : indicate_inter_apply, indicate_inter_apply, mul_mul_mul_comm, prod_mul_distrib] simp [c, indicate_inf_apply, ← translate_indicate, sub_eq_add_neg, mul_assoc, add_comm] -private lemma sum_c (p : ℕ) (B A : Finset G) : ∑ s, (B ∩ c p A s).card = A.card ^ p * B.card := by +private lemma sum_c (p : ℕ) (B A : Finset G) : ∑ s, #(B ∩ c p A s) = #A ^ p * #B := by simp only [card_eq_sum_indicate, indicate_inter_apply, c, indicate_inf_apply, mul_sum, sum_mul, sum_pow', @sum_comm G, Fintype.piFinset_univ, ← translate_indicate, translate_apply] congr with x exact Fintype.sum_equiv (Equiv.subLeft fun _ ↦ x) _ _ fun s ↦ mul_comm _ _ private lemma sum_cast_c (p : ℕ) (B A : Finset G) : - ∑ s, ((B ∩ c p A s).card : ℝ) = A.card ^ p * B.card := by + ∑ s, (#(B ∩ c p A s) : ℝ) = #A ^ p * #B := by rw [← Nat.cast_sum, sum_c]; norm_cast variable [MeasurableSpace G] noncomputable def s (p : ℝ≥0) (ε : ℝ) (B₁ B₂ A : Finset G) : Finset G := - univ.filter fun x ↦ (1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] < (𝟭 A ○ 𝟭 A) x + {x | (1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] < (𝟭 A ○ 𝟭 A) x} @[simp] lemma mem_s {p : ℝ≥0} {ε : ℝ} {B₁ B₂ A : Finset G} {x : G} : @@ -76,16 +76,16 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ ∃ A₁, A₁ ⊆ B₁ ∧ ∃ A₂, A₂ ⊆ B₂ ∧ ⟪μ_[ℝ] A₁ ○ μ A₂, (↑) ∘ f⟫_[ℝ] * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p ≤ 2 * ∑ x, (μ B₁ ○ μ B₂) x * (𝟭_[ℝ] A ○ 𝟭 A) x ^ p * f x ∧ - (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p) - ≤ A₁.card / B₁.card ∧ - (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p) - ≤ A₂.card / B₂.card := by + (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) + ≤ #A₁ / #B₁ ∧ + (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) + ≤ #A₂ / #B₂ := by have := hB.mono inter_subset_left have := hB.mono inter_subset_right have hp₀ : p ≠ 0 := by positivity have := dLpNorm_conv_pos hp₀ hB hA set M : ℝ := - 2 ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p * (sqrt B₁.card * sqrt B₂.card) / A.card ^ p + 2 ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p * (sqrt #B₁ * sqrt #B₂) / #A ^ p with hM_def have hM : 0 < M := by rw [hM_def]; positivity replace hf : 0 < ∑ x, (μ_[ℝ] B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x := by @@ -98,16 +98,16 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ forall_const, Set.mem_inter_iff, ← coe_sub, mem_coe, support_pow' _ hp₀, hf] set A₁ := fun s ↦ B₁ ∩ c p A s set A₂ := fun s ↦ B₂ ∩ c p A s - set g : (Fin p → G) → ℝ := fun s ↦ (A₁ s).card * (A₂ s).card with hg_def + set g : (Fin p → G) → ℝ := fun s ↦ #(A₁ s) * #(A₂ s) with hg_def have hg : ∀ s, 0 ≤ g s := fun s ↦ by rw [hg_def]; dsimp; positivity - have hgB : ∑ s, g s = B₁.card * B₂.card * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p := by + have hgB : ∑ s, g s = #B₁ * #B₂ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p := by have hAdconv : 0 ≤ 𝟭_[ℝ] A ○ 𝟭 A := dconv_nonneg indicate_nonneg indicate_nonneg simpa only [wLpNorm_pow_eq_sum_norm hp₀, wInner_one_eq_sum, sum_dconv, sum_indicate, Pi.one_apply, RCLike.inner_apply, RCLike.conj_to_real, norm_of_nonneg (hAdconv _), mul_one, nsmul_eq_mul, Nat.cast_mul, ← hg_def, NNReal.smul_def, NNReal.coe_dconv, NNReal.coe_comp_mu] using lemma_0 p B₁ B₂ A 1 suffices ∑ s, ⟪𝟭_[ℝ] (A₁ s) ○ 𝟭 (A₂ s), (↑) ∘ f⟫_[ℝ] * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p - < ∑ s, 𝟭 (univ.filter fun s ↦ M ^ 2 ≤ g s) s * g s * + < ∑ s, 𝟭 ({s | M ^ 2 ≤ g s} : Finset _) s * g s * (2 * ∑ x, (μ B₁ ○ μ B₂) x * (𝟭_[ℝ] A ○ 𝟭 A) x ^ p * f x) by obtain ⟨s, -, hs⟩ := exists_lt_of_sum_lt this refine ⟨_, inter_subset_left (s₂ := c p A s), _, inter_subset_left (s₂ := c p A s), ?_⟩ @@ -119,8 +119,8 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ -- positivity cases hs.not_le $ mul_nonneg (sum_nonneg fun x _ ↦ mul_nonneg (this _) $ by positivity) $ by positivity - have : (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p) - ≤ (A₁ s).card / B₁.card * ((A₂ s).card / B₂.card) := by + have : (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) + ≤ #(A₁ s) / #B₁ * (#(A₂ s) / #B₂) := by rw [div_mul_div_comm, le_div_iff₀] simpa [hg_def, hM_def, mul_pow, div_pow, pow_mul', show (2 : ℝ) ^ 2 = 4 by norm_num, mul_div_right_comm] using h @@ -152,15 +152,14 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ calc ∑ s with g s < M ^ 2, g s = ∑ s with g s < M ^ 2 ∧ g s ≠ 0, sqrt (g s) * sqrt (g s) := by simp_rw [mul_self_sqrt (hg _), ← filter_filter, sum_filter_ne_zero] - _ < ∑ s with g s < M ^ 2 ∧ g s ≠ 0, M * sqrt (g s) - := 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).card * sqrt (A₂ s).card) - := by simp_rw [mul_sum, sqrt_mul $ Nat.cast_nonneg _] - _ ≤ M * (sqrt (∑ s, (A₁ s).card) * sqrt (∑ s, (A₂ s).card)) - := mul_le_mul_of_nonneg_left - (sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity) hM.le - _ = _ := ?_ + _ < ∑ s with g s < M ^ 2 ∧ g s ≠ 0, M * sqrt (g s) + := 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 _] + _ ≤ 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 + _ = _ := ?_ · simp only [mem_filter, mem_univ, true_and, Nat.cast_nonneg, and_imp] exact fun s hsM hs ↦ mul_lt_mul_of_pos_right ((sqrt_lt' hM).2 hsM) $ sqrt_pos.2 $ (hg _).lt_of_ne' hs @@ -174,21 +173,20 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 (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 ∧ - (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p) ≤ - A₁.card / B₁.card ∧ - (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p) ≤ - A₂.card / B₂.card := by + (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) ≤ + #A₁ / #B₁ ∧ + (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) ≤ + #A₂ / #B₂ := by obtain ⟨A₁, hAB₁, A₂, hAB₂, h, hcard₁, hcard₂⟩ := drc hp₂ (𝟭 (s p ε B₁ B₂ A)ᶜ) (by simpa only [support_indicate, coe_compl, Set.mem_compl_iff, mem_coe]) hB hA refine ⟨A₁, hAB₁, A₂, hAB₂, ?_, hcard₁, hcard₂⟩ have hp₀ : 0 < p := by positivity - have aux : - ∀ (c : Finset G) (r), - (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p) ≤ c.card / r → - c.Nonempty := by + have aux (c : Finset G) (r) + (h : (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) ≤ #c / r) : + c.Nonempty := by simp_rw [nonempty_iff_ne_empty] - rintro c r h rfl + rintro rfl simp [pow_mul', (zero_lt_four' ℝ).not_le, inv_mul_le_iff₀ (zero_lt_four' ℝ), mul_assoc, div_nonpos_iff, mul_nonpos_iff, (pow_pos (dLpNorm_conv_pos hp₀.ne' hB hA) 2).not_le] at h norm_cast at h @@ -247,7 +245,7 @@ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p · have hp₀ : p ≠ 0 := by positivity have : (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤ - 4⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ univ] ^ (2 * p) / A.card ^ (2 * p) := by + 4⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ univ] ^ (2 * p) / #A ^ (2 * p) := by rw [mul_div_assoc, ← div_pow] refine mul_le_mul_of_nonneg_left (pow_le_pow_left (by positivity) ?_ _) (by norm_num) rw [nnratCast_dens, le_div_iff₀, ← mul_div_right_comm] diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index 1582476ae4..487c5df1d6 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/LeanAPAP/Physics/Unbalancing.lean @@ -28,7 +28,7 @@ lemma pow_inner_nonneg' {f : G → ℂ} (hf : g ○ g = f) (hν : h ○ h = (↑ simp only [WithLp.equiv_symm_pi_apply, Pi.pow_apply, RCLike.inner_apply, map_pow] simp_rw [dconv_apply h, mul_sum] --TODO: Please make `conv` work here :( - have : ∀ x, ∀ yz ∈ univ.filter fun yz : G × G ↦ yz.1 - yz.2 = x, + have : ∀ x, ∀ yz ∈ ({yz : G × G | yz.1 - yz.2 = x} : Finset _), conj ((g ○ g) x) ^ k * (h yz.1 * conj (h yz.2)) = conj ((g ○ g) (yz.1 - yz.2)) ^ k * (h yz.1 * conj (h yz.2)) := by simp only [mem_filter, mem_univ, true_and] @@ -100,8 +100,8 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 pow_sub_one_mul hp₁.pos.ne', NNReal.smul_def, smul_eq_mul] · simp [wInner_one_eq_sum, ← sum_add_distrib, ← mul_add, ← pow_sub_one_mul hp₁.pos.ne' (f _), mul_sum, mul_left_comm (2 : ℝ), add_abs_eq_two_nsmul_posPart] - set P := univ.filter fun i ↦ 0 ≤ f i - set T := univ.filter fun i ↦ 3 / 4 * ε ≤ f i + 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 rw [inv_mul_le_iff₀ (zero_lt_two' ℝ), sum_filter] diff --git a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean index e22240be06..b3b2127eac 100644 --- a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean +++ b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean @@ -101,7 +101,7 @@ def mkZModAux {ι : Type} [DecidableEq ι] (n : ι → ℕ) (u : ∀ i, ZMod (n lemma mkZModAux_injective {ι : Type} [DecidableEq ι] {n : ι → ℕ} (hn : ∀ i, n i ≠ 0) : Injective (mkZModAux n) := - AddChar.directSum_injective.comp fun f g h ↦ by simpa [Function.funext_iff, hn] using h + AddChar.directSum_injective.comp fun f g h ↦ by simpa [funext_iff, hn] using h /-- The circle-valued characters of a finite abelian group are the same as its complex-valued characters. -/ diff --git a/LeanAPAP/Prereqs/Bohr/Basic.lean b/LeanAPAP/Prereqs/Bohr/Basic.lean index 5844c931d8..5b0d6320af 100644 --- a/LeanAPAP/Prereqs/Bohr/Basic.lean +++ b/LeanAPAP/Prereqs/Bohr/Basic.lean @@ -2,7 +2,7 @@ import Mathlib.Analysis.Complex.Basic import LeanAPAP.Prereqs.AddChar.PontryaginDuality open AddChar Function -open scoped NNReal ENNReal +open scoped NNReal ENNReal Finset /-- A *Bohr set* `B` on an additive group `G` is a finite set of characters of `G`, called the *frequencies*, along with an extended non-negative real number for each frequency `ψ`, called the @@ -233,9 +233,9 @@ noncomputable instance [Finite G] : CompletelyDistribLattice (BohrSet G) := /-! ### Width, frequencies, rank -/ /-- The rank of a Bohr set is the number of characters which have finite width. -/ -def rank (B : BohrSet G) : ℕ := B.frequencies.card +def rank (B : BohrSet G) : ℕ := #B.frequencies -@[simp] lemma card_frequencies (B : BohrSet G) : B.frequencies.card = B.rank := rfl +@[simp] lemma card_frequencies (B : BohrSet G) : #B.frequencies = B.rank := rfl /-! ### Dilation -/ diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean index 31f47c7b37..89275b97cd 100644 --- a/LeanAPAP/Prereqs/Chang.lean +++ b/LeanAPAP/Prereqs/Chang.lean @@ -55,7 +55,7 @@ end Mathlib.Meta.Positivity lemma AddDissociated.boringEnergy_le [DecidableEq G] {s : Finset G} (hs : AddDissociated (s : Set G)) (n : ℕ) : - boringEnergy n s ≤ changConst ^ n * n ^ n * s.card ^ n := by + boringEnergy n s ≤ changConst ^ n * n ^ n * #s ^ n := by obtain rfl | hn := eq_or_ne n 0 · simp calc @@ -87,14 +87,14 @@ private lemma α_le_one (f : G → ℂ) : ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / ca lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x ≠ 0 → 1 ≤ ν x) (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0) : - ↑Δ.card ^ (2 * m) * (η ^ (2 * m) * (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2)) ≤ + #Δ ^ (2 * m) * (η ^ (2 * m) * (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2)) ≤ energy m Δ (dft fun a ↦ ν a) := by obtain rfl | hf := eq_or_ne f 0 · simp choose c norm_c hc using fun γ ↦ RCLike.exists_norm_eq_mul_self (dft f γ) have := calc - η * ‖f‖_[1] * Δ.card ≤ ∑ γ in Δ, ‖dft f γ‖ := ?_ + η * ‖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] @@ -156,7 +156,7 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x open scoped ComplexOrder lemma spec_hoelder (hη : 0 ≤ η) (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0) : - Δ.card ^ (2 * m) * (η ^ (2 * m) * (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)) ≤ boringEnergy m Δ := by + #Δ ^ (2 * m) * (η ^ (2 * m) * (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)) ≤ boringEnergy m Δ := by have hG : (0 : ℝ) < card G := by positivity simpa [boringEnergy, mul_assoc, ← Pi.one_def, ← mul_div_right_comm, ← mul_div_assoc, div_le_iff₀ hG, energy_nsmul, -nsmul_eq_mul, ← nsmul_eq_mul'] using @@ -165,10 +165,10 @@ lemma spec_hoelder (hη : 0 ≤ η) (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0) /-- **Chang's lemma**. -/ lemma chang (hf : f ≠ 0) (hη : 0 < η) : ∃ Δ, Δ ⊆ largeSpec f η ∧ - Δ.card ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)⌉₊ / η ^ 2⌉₊ ∧ + #Δ ≤ ⌈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 _ _ Δ.card + obtain hΔ' | hΔ' := @eq_zero_or_pos _ _ #Δ · simp [hΔ'] let α := ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G have : 0 < α := by positivity @@ -176,16 +176,16 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) : have hβ : 0 < β := Nat.ceil_pos.2 (curlog_pos (by positivity) $ α_le_one _) have : 0 < ‖f‖_[1] := by positivity refine le_of_pow_le_pow_left hβ.ne' zero_le' $ Nat.cast_le.1 $ le_of_mul_le_mul_right ?_ - (by positivity : 0 < Δ.card ^ β * (η ^ (2 * β) * α)) + (by positivity : 0 < #Δ ^ β * (η ^ (2 * β) * α)) push_cast rw [← mul_assoc, ← pow_add, ← two_mul] refine ((spec_hoelder hη.le hΔη hβ.ne').trans $ hΔ.boringEnergy_le _).trans ?_ refine le_trans ?_ $ mul_le_mul_of_nonneg_right (pow_le_pow_left ?_ (Nat.le_ceil _) _) ?_ rw [mul_right_comm, div_pow, mul_pow, mul_pow, exp_one_pow, ← pow_mul, mul_div_assoc] calc - _ = (changConst * Δ.card * β) ^ β := by ring - _ ≤ (changConst * Δ.card * β) ^ β * (α * exp β) := ?_ - _ ≤ (changConst * Δ.card * β) ^ β * ((η / η) ^ (2 * β) * α * exp β) := by + _ = (changConst * #Δ * β) ^ β := by ring + _ ≤ (changConst * #Δ * β) ^ β * (α * exp β) := ?_ + _ ≤ (changConst * #Δ * β) ^ β * ((η / η) ^ (2 * β) * α * exp β) := by rw [div_self hη.ne', one_pow, one_mul] _ = _ := by ring refine le_mul_of_one_le_right (by positivity) ?_ diff --git a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean index 22245f4799..1a343be73b 100644 --- a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean +++ b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean @@ -52,7 +52,7 @@ section CommSemiring variable [CommSemiring R] {f g : G → R} lemma indicate_conv_indicate_eq_sum (s t : Finset G) (a : G) : - (𝟭_[R] s ∗ 𝟭 t) a = ((s ×ˢ t).filter fun x : G × G ↦ x.1 + x.2 = a).card := by + (𝟭_[R] s ∗ 𝟭 t) a = #{x ∈ s ×ˢ t | x.1 + x.2 = a} := by simp only [conv_apply, indicate_apply, ← ite_and, filter_comm, boole_mul, sum_boole] simp_rw [← mem_product, filter_univ_mem] @@ -63,7 +63,7 @@ lemma conv_indicate (f : G → R) (s : Finset G) : f ∗ 𝟭 s = ∑ a ∈ s, ext; simp [conv_eq_sum_sub, indicate_apply] lemma indicate_conv_indicate_eq_card_vadd_inter_neg (s t : Finset G) (a : G) : - (𝟭_[R] s ∗ 𝟭 t) a = ((-a +ᵥ s) ∩ -t).card := by + (𝟭_[R] s ∗ 𝟭 t) a = #((-a +ᵥ s) ∩ -t) := by rw [← card_neg, neg_inter] simp [conv_indicate, indicate, inter_comm, ← filter_mem_eq_inter, ← neg_vadd_mem_iff, ← sub_eq_add_neg] @@ -71,7 +71,7 @@ lemma indicate_conv_indicate_eq_card_vadd_inter_neg (s t : Finset G) (a : G) : variable [StarRing R] lemma indicate_dconv_indicate_apply (s t : Finset G) (a : G) : - (𝟭_[R] s ○ 𝟭 t) a = ((s ×ˢ t).filter fun x : G × G ↦ x.1 - x.2 = a).card := by + (𝟭_[R] s ○ 𝟭 t) a = #{x ∈ s ×ˢ t | x.1 - x.2 = a} := by simp only [dconv_apply, indicate_apply, ← ite_and, filter_comm, boole_mul, sum_boole, apply_ite conj, map_one, map_zero, Pi.conj_apply] simp_rw [← mem_product, filter_univ_mem] @@ -90,10 +90,10 @@ variable [Semifield R] @[simp] lemma mu_univ_conv_mu_univ : μ_[R] (univ : Finset G) ∗ μ univ = μ univ := by ext; cases eq_or_ne (card G : R) 0 <;> simp [mu_apply, conv_eq_sum_add, card_univ, *] -lemma mu_conv (s : Finset G) (f : G → R) : μ s ∗ f = (s.card : R)⁻¹ • ∑ a ∈ s, τ a f := by +lemma mu_conv (s : Finset G) (f : G → R) : μ s ∗ f = (#s : R)⁻¹ • ∑ a ∈ s, τ a f := by simp [mu, indicate_conv, smul_conv] -lemma conv_mu (f : G → R) (s : Finset G) : f ∗ μ s = (s.card : R)⁻¹ • ∑ a ∈ s, τ a f := by +lemma conv_mu (f : G → R) (s : Finset G) : f ∗ μ s = (#s : R)⁻¹ • ∑ a ∈ s, τ a f := by simp [mu, conv_indicate, conv_smul] variable [StarRing R] @@ -102,10 +102,10 @@ variable [StarRing R] ext; cases eq_or_ne (card G : R) 0 <;> simp [mu_apply, dconv_eq_sum_add, card_univ, *] lemma mu_dconv (s : Finset G) (f : G → R) : - μ s ○ f = (s.card : R)⁻¹ • ∑ a ∈ s, τ a (conjneg f) := by + μ s ○ f = (#s : R)⁻¹ • ∑ a ∈ s, τ a (conjneg f) := by simp [mu, indicate_dconv, smul_dconv] -lemma dconv_mu (f : G → R) (s : Finset G) : f ○ μ s = (s.card : R)⁻¹ • ∑ a ∈ s, τ (-a) f := by +lemma dconv_mu (f : G → R) (s : Finset G) : f ○ μ s = (#s : R)⁻¹ • ∑ a ∈ s, τ (-a) f := by simp [mu, dconv_indicate, dconv_smul] end Semifield @@ -150,7 +150,7 @@ section CommSemiring variable [CommSemiring R] {f g : G → R} {n : ℕ} lemma indicate_iterConv_apply (s : Finset G) (n : ℕ) (a : G) : - (𝟭_[R] s ∗^ n) a = ((s ^^ n).filter fun x : Fin n → G ↦ ∑ i, x i = a).card := by + (𝟭_[R] s ∗^ n) a = #{x ∈ s ^^ n | ∑ i, x i = a} := by induction' n with n ih generalizing a · simp [apply_ite card, eq_comm] simp_rw [iterConv_succ', conv_eq_sum_sub', ih, indicate_apply, boole_mul, sum_ite, diff --git a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean index fcf911c061..ea0c1a1e86 100644 --- a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean +++ b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean @@ -15,12 +15,12 @@ variable {G : Type*} [AddCommGroup G] [DecidableEq G] [Fintype G] {s : Finset G} lemma ThreeAPFree.wInner_one_mu_conv_mu_mu_two_smul_mu (hG : Odd (card G)) (hs : ThreeAPFree (s : Set G)) : - ⟪μ_[ℝ] s ∗ μ s, μ (s.image (2 • ·))⟫_[ℝ] = (s.card ^ 2 : ℝ)⁻¹ := by + ⟪μ_[ℝ] s ∗ μ s, μ (s.image (2 • ·))⟫_[ℝ] = (#s ^ 2 : ℝ)⁻¹ := by obtain rfl | hs' := s.eq_empty_or_nonempty · simp simp only [wInner_one_eq_sum, inner_apply, sum_conv_mul, ← sum_product', RCLike.conj_to_real] rw [← diag_union_offDiag univ, sum_union (disjoint_diag_offDiag _), sum_diag, ← - sum_add_sum_compl s, @sum_eq_card_nsmul _ _ _ _ _ (s.card ^ 3 : ℝ)⁻¹, nsmul_eq_mul, + sum_add_sum_compl s, @sum_eq_card_nsmul _ _ _ _ _ (#s ^ 3 : ℝ)⁻¹, nsmul_eq_mul, Finset.sum_eq_zero, Finset.sum_eq_zero, add_zero, add_zero, pow_succ', mul_inv, mul_inv_cancel_left₀] · exact Nat.cast_ne_zero.2 hs'.card_pos.ne' diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean index 8a48e2ebdc..c4722564be 100644 --- a/LeanAPAP/Prereqs/Energy.lean +++ b/LeanAPAP/Prereqs/Energy.lean @@ -42,7 +42,7 @@ lemma boringEnergy_eq (n : ℕ) (s : Finset G) : boringEnergy n s = ∑ x, (𝟭 refine sum_congr rfl fun f hf ↦ ?_ simp_rw [(mem_filter.1 hf).2, eq_comm] -@[simp] lemma boringEnergy_one (s : Finset G) : boringEnergy 1 s = s.card := by +@[simp] lemma boringEnergy_one (s : Finset G) : boringEnergy 1 s = #s := by simp [boringEnergy_eq, indicate_apply] lemma cLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) : @@ -63,7 +63,7 @@ lemma cLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) : Nat.cast_eq_zero, Fintype.card_ne_zero, or_false, sq, Complex.ofReal_iterConv, (((indicate_isSelfAdjoint _).iterConv _).apply _).conj_eq, Complex.ofReal_comp_indicate] -lemma cL2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt s.card := by +lemma cL2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt #s := by rw [eq_comm, sqrt_eq_iff_eq_sq, eq_comm] simpa using cLpNorm_dft_indicate_pow 1 s all_goals positivity diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean index 0c21e5a123..0a677f1897 100644 --- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean +++ b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean @@ -119,7 +119,7 @@ lemma dft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime variable [DecidableEq α] -@[simp] lemma dft_indicate_zero (A : Finset α) : dft (𝟭 A) 0 = A.card := by +@[simp] lemma dft_indicate_zero (A : Finset α) : dft (𝟭 A) 0 = #A := by simp only [dft_apply, wInner_one_eq_sum, inner_apply, sum_indicate, AddChar.zero_apply, map_one, one_mul] diff --git a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean index 43343ab2f2..2807a8554e 100644 --- a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean +++ b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean @@ -36,7 +36,7 @@ end CommSemiring section Semifield variable [Fintype ι] [DecidableEq ι] [Semiring β] [Module ℚ≥0 β] -lemma expect_indicate (s : Finset ι) : 𝔼 x, 𝟭_[β] s x = s.card /ℚ Fintype.card ι := by +lemma expect_indicate (s : Finset ι) : 𝔼 x, 𝟭_[β] s x = #s /ℚ Fintype.card ι := by simp only [expect_univ, indicate] rw [← sum_filter, filter_mem_eq_inter, univ_inter, sum_const, Nat.smul_one_eq_cast] diff --git a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean index bbc1199109..3aad71670b 100644 --- a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean +++ b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean @@ -61,9 +61,9 @@ variable (β) end Nontrivial -lemma sum_indicate [Fintype α] (s : Finset α) : ∑ x, 𝟭_[β] s x = s.card := by simp [indicate_apply] +lemma sum_indicate [Fintype α] (s : Finset α) : ∑ x, 𝟭_[β] s x = #s := by simp [indicate_apply] -lemma card_eq_sum_indicate [Fintype α] (s : Finset α) : s.card = ∑ x, 𝟭_[ℕ] s x := +lemma card_eq_sum_indicate [Fintype α] (s : Finset α) : #s = ∑ x, 𝟭_[ℕ] s x := (sum_indicate _ _).symm section AddGroup @@ -126,7 +126,7 @@ variable [OrderedSemiring β] {s : Finset α} @[simp] lemma indicate_nonneg : 0 ≤ 𝟭_[β] s := fun a ↦ by rw [indicate_apply]; split_ifs <;> simp @[simp] lemma indicate_pos [Nontrivial β] : 0 < 𝟭_[β] s ↔ s.Nonempty := by - simp [indicate_apply, Pi.lt_def, Function.funext_iff, lt_iff_le_and_ne, @eq_comm β 0, + simp [indicate_apply, Pi.lt_def, funext_iff, lt_iff_le_and_ne, @eq_comm β 0, Finset.Nonempty] protected alias ⟨_, Finset.Nonempty.indicate_pos⟩ := indicate_pos @@ -139,13 +139,13 @@ section DivisionSemiring variable [DivisionSemiring β] [DivisionSemiring γ] {s : Finset α} /-- The normalised indicate of a set. -/ -def mu (s : Finset α) : α → β := (s.card : β)⁻¹ • 𝟭 s +def mu (s : Finset α) : α → β := (#s : β)⁻¹ • 𝟭 s notation "μ " => mu notation "μ_[" β "] " => @mu _ β _ _ -lemma mu_apply (x : α) : μ s x = (s.card : β)⁻¹ * ite (x ∈ s) 1 0 := rfl +lemma mu_apply (x : α) : μ s x = (#s : β)⁻¹ * ite (x ∈ s) 1 0 := rfl @[simp] lemma mu_empty : (μ ∅ : α → β) = 0 := by ext; simp [mu] @@ -166,7 +166,7 @@ variable [CharZero β] {a : α} lemma mu_apply_ne_zero : μ_[β] s a ≠ 0 ↔ a ∈ s := mu_apply_eq_zero.not_left @[simp] lemma mu_eq_zero : μ_[β] s = 0 ↔ s = ∅ := by - simp [Function.funext_iff, eq_empty_iff_forall_not_mem] + simp [funext_iff, eq_empty_iff_forall_not_mem] lemma mu_ne_zero : μ_[β] s ≠ 0 ↔ s.Nonempty := mu_eq_zero.not.trans nonempty_iff_ne_empty.symm @@ -179,7 +179,7 @@ end Nontrivial variable (β) -lemma card_smul_mu [CharZero β] (s : Finset α) : s.card • μ_[β] s = 𝟭 s := by +lemma card_smul_mu [CharZero β] (s : Finset α) : #s • μ_[β] s = 𝟭 s := by ext x : 1 rw [Pi.smul_apply, mu_apply, indicate_apply, nsmul_eq_mul] split_ifs with h @@ -188,7 +188,7 @@ lemma card_smul_mu [CharZero β] (s : Finset α) : s.card • μ_[β] s = 𝟭 s exact ⟨_, h⟩ · rw [mul_zero, mul_zero] -lemma card_smul_mu_apply [CharZero β] (s : Finset α) (x : α) : s.card • μ_[β] s x = 𝟭 s x := +lemma card_smul_mu_apply [CharZero β] (s : Finset α) (x : α) : #s • μ_[β] s x = 𝟭 s x := congr_fun (card_smul_mu β _) _ @[simp] lemma sum_mu [CharZero β] [Fintype α] (hs : s.Nonempty) : ∑ x, μ_[β] s x = 1 := by diff --git a/LeanAPAP/Prereqs/LargeSpec.lean b/LeanAPAP/Prereqs/LargeSpec.lean index c45bda0642..56fe40b1d7 100644 --- a/LeanAPAP/Prereqs/LargeSpec.lean +++ b/LeanAPAP/Prereqs/LargeSpec.lean @@ -12,7 +12,7 @@ variable {G : Type*} [AddCommGroup G] [Fintype G] [MeasurableSpace G] {f : G → /-- The `η`-large spectrum of a function. -/ noncomputable def largeSpec (f : G → ℂ) (η : ℝ) : Finset (AddChar G ℂ) := - univ.filter fun ψ ↦ η * ‖f‖_[1] ≤ ‖dft f ψ‖ + {ψ | η * ‖f‖_[1] ≤ ‖dft f ψ‖} @[simp] lemma mem_largeSpec : ψ ∈ largeSpec f η ↔ η * ‖f‖_[1] ≤ ‖dft f ψ‖ := by simp [largeSpec] diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean index ea19dd2c7e..610ebb43c4 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean @@ -18,33 +18,33 @@ variable {ι G 𝕜 E R : Type*} [Fintype ι] {mι : MeasurableSpace ι} [Discre section Indicator variable [RCLike R] [DecidableEq ι] {s : Finset ι} {p : ℝ≥0} -lemma dLpNorm_rpow_indicate (hp : p ≠ 0) (s : Finset ι) : ‖𝟭_[R] s‖_[p] ^ (p : ℝ) = s.card := by +lemma dLpNorm_rpow_indicate (hp : p ≠ 0) (s : Finset ι) : ‖𝟭_[R] s‖_[p] ^ (p : ℝ) = #s := by have : ∀ x, (ite (x ∈ s) 1 0 : ℝ) ^ (p : ℝ) = ite (x ∈ s) (1 ^ (p : ℝ)) (0 ^ (p : ℝ)) := fun x ↦ by split_ifs <;> simp simp [dLpNorm_rpow_eq_sum_nnnorm, hp, indicate_apply, apply_ite nnnorm, -sum_const, card_eq_sum_ones, sum_boole, this, zero_rpow, filter_mem_eq_inter] -lemma dLpNorm_indicate (hp : p ≠ 0) (s : Finset ι) : ‖𝟭_[R] s‖_[p] = s.card ^ (p⁻¹ : ℝ) := by +lemma dLpNorm_indicate (hp : p ≠ 0) (s : Finset ι) : ‖𝟭_[R] s‖_[p] = #s ^ (p⁻¹ : ℝ) := by refine (NNReal.eq_rpow_inv_iff ?_).2 (dLpNorm_rpow_indicate ?_ _) <;> positivity lemma dLpNorm_pow_indicate {p : ℕ} (hp : p ≠ 0) (s : Finset ι) : - ‖𝟭_[R] s‖_[p] ^ (p : ℝ) = s.card := by + ‖𝟭_[R] s‖_[p] ^ (p : ℝ) = #s := by simpa using dLpNorm_rpow_indicate (Nat.cast_ne_zero.2 hp) s -lemma dL2Norm_sq_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[2] ^ 2 = s.card := by +lemma dL2Norm_sq_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[2] ^ 2 = #s := by simpa using dLpNorm_pow_indicate two_ne_zero s -@[simp] lemma dL2Norm_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[2] = NNReal.sqrt s.card := by +@[simp] lemma dL2Norm_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[2] = NNReal.sqrt #s := by rw [eq_comm, NNReal.sqrt_eq_iff_eq_sq, dL2Norm_sq_indicate] -@[simp] lemma dL1Norm_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[1] = s.card := by +@[simp] lemma dL1Norm_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[1] = #s := by simpa using dLpNorm_pow_indicate one_ne_zero s -lemma dLpNorm_mu (hp : 1 ≤ p) (hs : s.Nonempty) : ‖μ_[R] s‖_[p] = s.card ^ ((p : ℝ)⁻¹ - 1) := by - rw [mu, dLpNorm_const_smul (s.card⁻¹ : R) (𝟭_[R] s), dLpNorm_indicate, nnnorm_inv, +lemma dLpNorm_mu (hp : 1 ≤ p) (hs : s.Nonempty) : ‖μ_[R] s‖_[p] = #s ^ ((p : ℝ)⁻¹ - 1) := by + rw [mu, dLpNorm_const_smul ((#s)⁻¹ : R) (𝟭_[R] s), dLpNorm_indicate, nnnorm_inv, RCLike.nnnorm_natCast, inv_mul_eq_div, ← NNReal.rpow_sub_one] <;> positivity -lemma dLpNorm_mu_le (hp : 1 ≤ p) : ‖μ_[R] s‖_[p] ≤ s.card ^ (p⁻¹ - 1 : ℝ) := by +lemma dLpNorm_mu_le (hp : 1 ≤ p) : ‖μ_[R] s‖_[p] ≤ #s ^ (p⁻¹ - 1 : ℝ) := by obtain rfl | hs := s.eq_empty_or_nonempty · simp · exact (dLpNorm_mu hp hs).le @@ -54,7 +54,7 @@ lemma dLpNorm_mu_le (hp : 1 ≤ p) : ‖μ_[R] s‖_[p] ≤ s.card ^ (p⁻¹ - 1 lemma dL1Norm_mu_le_one : ‖μ_[R] s‖_[1] ≤ 1 := by simpa using dLpNorm_mu_le le_rfl -@[simp] lemma dL2Norm_mu (hs : s.Nonempty) : ‖μ_[R] s‖_[2] = s.card ^ (-2⁻¹ : ℝ) := by +@[simp] lemma dL2Norm_mu (hs : s.Nonempty) : ‖μ_[R] s‖_[2] = #s ^ (-2⁻¹ : ℝ) := by have : (2⁻¹ - 1 : ℝ) = -2⁻¹ := by norm_num simpa [sqrt_eq_rpow, this] using dLpNorm_mu one_le_two (R := R) hs diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean index 96d1c94d22..a1d3d70b3a 100644 --- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean +++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean @@ -22,30 +22,30 @@ 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) : |∑ i, f (a i)| ^ (m + 1) ≤ - (∑ b in A ^^ n, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / A.card ^ n := by + (∑ b in 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.card)| ^ (m + 1) := by + = |∑ i, (f (a i) - (∑ b in 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.card| ^ (m + 1) := by + _ = |(∑ b in 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.card ^ (m + 1) := by + _ = |∑ b in 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.card ^ (m + 1) := by + _ ≤ (∑ b in 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.card ^ m / B.card := by + _ = (∑ b in 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.card := by + _ ≤ (∑ b in 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 : ℕ) (a : Fin n → ι) : - |∑ i, f (a i)| ^ m ≤ (∑ b in A ^^ n, |∑ i, (f (a i) - f (b i))| ^ m) / A.card ^ n := by + |∑ i, f (a i)| ^ m ≤ (∑ b in 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] @@ -162,14 +162,14 @@ private lemma step_eight {f : ι → ℝ} {a b : Fin n → ι} : private lemma end_step {f : ι → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) : (∑ a in A ^^ n, ∑ b in A ^^ n, ∑ k in piAntidiag univ m, - ↑(multinomial univ fun i ↦ 2 * k i) * ∏ t, (f (a t) - f (b t)) ^ (2 * k t)) / A.card ^ n + ↑(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 let B := A ^^ n calc (∑ a in B, ∑ b in B, ∑ k : Fin n → ℕ in piAntidiag univ m, - (multinomial univ fun i ↦ 2 * k i : ℝ) * ∏ t, (f (a t) - f (b t)) ^ (2 * k t)) / A.card ^ n + (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)) * - ((∑ i, f (a i) ^ 2) ^ m + (∑ i, f (b i) ^ 2) ^ m) : ℝ) / A.card ^ n := by + ((∑ 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 simp only [mul_add, sum_add_distrib, sum_const, nsmul_eq_mul, ← mul_sum] @@ -194,7 +194,7 @@ theorem marcinkiewicz_zygmund' (m : ℕ) (f : ι → ℝ) (hf : ∀ i, ∑ a in 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.card ^ n := by + ≤ ∑ a in A ^^ n, (∑ b in 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] diff --git a/lake-manifest.json b/lake-manifest.json index d9cf40a63c..5a2d94e7e6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cc0bc876eeef0518ddc1c8d3bd6f48cc83e68901", + "rev": "eb6c831c05bc6ca6d37454ca97531a9b780dfcb5", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fa3d73a2cf077f4b14c7840352ac7b08aeb6eb41", + "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3", + "rev": "9ac12945862fa39eab7795c2f79bb9aa0c8e332c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12", + "rev": "0ea83a676d288220ba227808568cbb80fe43ace0", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d951eef6bb39b3b78cbd1fba9c515c3770a9d20a", + "rev": "d27f22898a74975360dd1387155c6031b501a90b", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,