diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index 780ef86de1..08b7cfea7d 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -86,11 +86,13 @@ end open Finset Real open scoped BigOperators Pointwise NNReal ENNReal -variable {G : Type*} [Fintype G] [MeasurableSpace G] [DiscreteMeasurableSpace G] {A S : Finset G} - {f : G → ℂ} {ε K : ℝ} {k m : ℕ} +variable {G : Type*} [Fintype G] {A S : Finset G} {f : G → ℂ} {ε K : ℝ} {k m : ℕ} + +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) ≤ + (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 have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two] have hm' : 2 * m ≠ 0 := by @@ -117,6 +119,8 @@ lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hk : 64 * m / ε ^ 2 ≤ k) : · norm_num1; exact hk positivity +end + variable [DecidableEq G] [AddCommGroup G] local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s @@ -135,7 +139,87 @@ lemma lemma28_part_one (hm : 1 ≤ m) (x : G) : rw [← sum_filter, filter_mem_eq_inter, univ_inter, sub_self, smul_zero] congr with a : 1 simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin] -variable [DecidableEq G] [AddCommGroup G] + +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 + 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 + 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 = + 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 + simp_rw [mul_sum, boole_mul, ← ite_and] + refine sum_congr rfl fun s₁ hs₁ ↦ ?_ + refine sum_congr rfl fun s₂ hs₂ ↦ ?_ + refine if_congr ?_ rfl rfl + rw [eq_sub_iff_add_eq', and_iff_right_of_imp] + intro h + simp only [mem_piDiag] at hs₁ hs₂ + have : x - y = s₂ - s₁ := by rw [sub_eq_sub_iff_add_eq_add, ← h, add_comm] + rw [this] + obtain ⟨i, -, rfl⟩ := hs₁ + 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, + 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 + 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 ?_ + · intro x _; split_ifs <;> norm_num + have := Fin.pos_iff_nonempty.1 (pos_iff_ne_zero.2 hk) + rw [card_piDiag] + simp only [nsmul_one] + refine this.trans ?_ + simp_rw [← sum_mul, mul_comm] + rfl + +-- might be true for dumb reason when k = 0, since L would be singleton and rhs is |G|, +-- so its just |S| ≤ |G| +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 + rcases S.eq_empty_or_nonempty with (rfl | hS) + · simpa only [card_empty, mul_zero, zero_le', and_true_iff] using hL' + have hS' : 0 < S.card := by rwa [card_pos] + have : (L + S.piDiag (Fin k)).card ≤ (A + S).card ^ k := by + refine (card_le_card (add_subset_add_right hL)).trans ?_ + rw [← Fintype.card_piFinset_const] + refine card_le_card fun i hi ↦ ?_ + simp only [mem_add, mem_piDiag, Fintype.mem_piFinset, exists_prop, exists_and_left, + exists_exists_and_eq_and] at hi ⊢ + 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 + · 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 + 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 + simp only [reindex_count L hk hL'] at this + rw [sq, mul_assoc, ← smul_eq_mul, mul_sum] at this + rw [← sum_const] at this + exact exists_le_of_sum_le hL' this + +variable [MeasurableSpace G] + namespace AlmostPeriodicity @@ -149,7 +233,7 @@ noncomputable def l (k m : ℕ) (ε : ℝ) (f : G → ℂ) (A : Finset G) : Fins lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m) (h : ∑ a in A ^^ k, - ‖fun x : G ↦ ∑ i : Fin k, f (x - a i) - (k • (mu A ∗ f)) x‖_[2 * m] ^ (2 * m) ≤ + (‖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 rw [← Nat.cast_pow, ← Fintype.card_piFinset_const] at h @@ -161,6 +245,8 @@ lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m) congr with a : 3 refine pow_le_pow_iff_left ?_ ?_ ?_ <;> positivity +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 @@ -169,7 +255,7 @@ lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) : have hm' : 1 < 2 * m := (Nat.mul_le_mul_left 2 hm).trans_lt' $ by norm_num1 have hm'' : (1 : ℝ≥0∞) ≤ 2 * m := by rw [← hmeq, Nat.one_le_cast]; exact hm'.le gcongr - refine (dLpNorm_sub_le hm'' _ _).trans ?_ + refine (dLpNorm_sub_le hm'').trans ?_ rw [dLpNorm_translate, two_mul ‖f‖_[2 * m], add_le_add_iff_left] have hmeq' : ((2 * m : ℝ≥0) : ℝ≥0∞) = 2 * m := by rw [ENNReal.coe_mul, ENNReal.coe_two, ENNReal.coe_natCast] @@ -194,7 +280,7 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) have hm' : 2 * m ≠ 0 := by linarith have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two] rw [← hmeq, mul_pow] - simp only [dLpNorm_pow_eq_sum_nnnorm hm'] + simp only [dLpNorm_pow_eq_sum_norm hm'] rw [sum_comm] have : ∀ x : G, ∑ a in A ^^ k, ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤ @@ -206,17 +292,17 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) simp only [@sum_comm _ _ G] have (a : Fin k → G) (i : Fin k) : ∑ x, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) = ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) := by - rw [← hmeq, dLpNorm_pow_eq_sum_nnnorm hm'] + rw [← hmeq, dLpNorm_pow_eq_sum_norm hm'] 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) := lemma28_part_two hm hA - refine this.trans ?_ + refine le_trans (mod_cast this) ?_ simp only [sum_const, Fintype.card_piFinset_const, nsmul_eq_mul, Nat.cast_pow] refine (lemma28_end hε hm hk).trans_eq' ?_ - simp only [mul_assoc, card_fin] + simp [mul_assoc, card_fin] lemma just_the_triangle_inequality {t : G} {a : Fin k → G} (ha : a ∈ l k m ε f A) (ha' : (a + fun _ ↦ t) ∈ l k m ε f A) (hk : 0 < k) (hm : 1 ≤ m) : @@ -245,88 +331,14 @@ lemma just_the_triangle_inequality {t : G} {a : Fin k → G} (ha : a ∈ l k m rwa [dLpNorm_sub_comm, ← h₄, ← h₃] have : (0 : ℝ) < k := by positivity refine le_of_mul_le_mul_left ?_ this - rw [← nsmul_eq_mul, ← dLpNorm_nsmul hp _ (_ - mu A ∗ f), nsmul_sub, ← + rw [← nsmul_eq_mul, ← NNReal.coe_nsmul, ← dLpNorm_nsmul _ (_ - mu A ∗ f), nsmul_sub, ← translate_smul_right (-t) (mu A ∗ f) k, mul_assoc, mul_left_comm, two_mul ((k : ℝ) * _), ← mul_assoc] - exact (dLpNorm_sub_le_dLpNorm_sub_add_dLpNorm_sub hp _ _).trans (add_le_add h₅₁ h₁) - -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 - 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 - 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 = - 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 - simp_rw [mul_sum, boole_mul, ← ite_and] - refine sum_congr rfl fun s₁ hs₁ ↦ ?_ - refine sum_congr rfl fun s₂ hs₂ ↦ ?_ - refine if_congr ?_ rfl rfl - rw [eq_sub_iff_add_eq', and_iff_right_of_imp] - intro h - simp only [mem_piDiag] at hs₁ hs₂ - have : x - y = s₂ - s₁ := by rw [sub_eq_sub_iff_add_eq_add, ← h, add_comm] - rw [this] - obtain ⟨i, -, rfl⟩ := hs₁ - 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, - 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 - 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 ?_ - · intro x _; split_ifs <;> norm_num - have := Fin.pos_iff_nonempty.1 (pos_iff_ne_zero.2 hk) - rw [card_piDiag] - simp only [nsmul_one] - refine this.trans ?_ - simp_rw [← sum_mul, mul_comm] - rfl - --- might be true for dumb reason when k = 0, since L would be singleton and rhs is |G|, --- so its just |S| ≤ |G| -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 - rcases S.eq_empty_or_nonempty with (rfl | hS) - · simpa only [card_empty, mul_zero, zero_le', and_true_iff] using hL' - have hS' : 0 < S.card := by rwa [card_pos] - have : (L + S.piDiag (Fin k)).card ≤ (A + S).card ^ k := by - refine (card_le_card (add_subset_add_right hL)).trans ?_ - rw [← Fintype.card_piFinset_const] - refine card_le_card fun i hi ↦ ?_ - simp only [mem_add, mem_piDiag, Fintype.mem_piFinset, exists_prop, exists_and_left, - exists_exists_and_eq_and] at hi ⊢ - 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 - · 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 - 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 - simp only [reindex_count L hk hL'] at this - rw [sq, mul_assoc, ← smul_eq_mul, mul_sum] at this - rw [← sum_const] at this - exact exists_le_of_sum_le hL' this + calc + (‖τ (-t) (k • (μ A ∗ f)) - k • (μ A ∗ f)‖_[2 * m] : ℝ) + ≤ ↑(‖τ (-t) (k • (μ A ∗ f)) - f₁‖_[2 * m] + ‖f₁ - k • (μ A ∗ f)‖_[2 * m]) := by + gcongr; exact dLpNorm_sub_le_dLpNorm_sub_add_dLpNorm_sub (mod_cast hp) + _ ≤ k * ε * ‖f‖_[2 * m] + k * ε * ‖f‖_[2 * m] := by push_cast; gcongr lemma T_bound (hK' : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ) * m / (ε / 2) ^ 2⌉₊) (h₁ : Lc * Sc ≤ ASc ^ k * Tc) (h₂ : (Ac : ℝ) ^ k / 2 ≤ Lc) (h₃ : (ASc : ℝ) ≤ K * Ac) @@ -384,7 +396,7 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) ( refine (mul_le_mul_of_nonneg_right this (Nat.cast_nonneg _)).trans ?_ rw [one_mul, Nat.cast_le] exact card_le_univ _ - simp only [mu_empty, zero_conv, translate_zero_right, sub_self, nnLpNorm_zero] + simp only [mu_empty, zero_conv, translate_zero_right, sub_self, dLpNorm_zero] positivity let k := ⌈(64 : ℝ) * m / (ε / 2) ^ 2⌉₊ have hk : k ≠ 0 := by positivity diff --git a/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean index 76aee26345..789728cfc6 100644 --- a/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean +++ b/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean @@ -53,8 +53,8 @@ variable [NormedField 𝕜] {p : ℝ≥0∞} {f g : α → 𝕜} lemma cLpNorm_const_smul [Module 𝕜 E] [BoundedSMul 𝕜 E] (c : 𝕜) (f : α → E) : ‖c • f‖ₙ_[p] = ‖c‖₊ * ‖f‖ₙ_[p] := by simp [cLpNorm, nnLpNorm_const_smul] -lemma cLpNorm_nsmul [NormedSpace ℝ E] (n : ℕ) (f : α → E) : ‖n • f‖ₙ_[p] = n • ‖f‖ₙ_[p] := by - simp [cLpNorm, nnLpNorm_nsmul] +lemma cLpNorm_nsmul [NormedSpace ℝ E] (n : ℕ) (f : α → E) (p : ℝ≥0∞) : + ‖n • f‖ₙ_[p] = n • ‖f‖ₙ_[p] := by simp [cLpNorm, nnLpNorm_nsmul] variable [NormedSpace ℝ 𝕜] diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean index b70259a10a..a36f061b6e 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean @@ -50,8 +50,8 @@ variable [NormedField 𝕜] {p : ℝ≥0∞} {f g : α → 𝕜} lemma dLpNorm_const_smul [Module 𝕜 E] [BoundedSMul 𝕜 E] (c : 𝕜) (f : α → E) : ‖c • f‖_[p] = ‖c‖₊ * ‖f‖_[p] := by simp [dLpNorm, nnLpNorm_const_smul] -lemma dLpNorm_nsmul [NormedSpace ℝ E] (n : ℕ) (f : α → E) : ‖n • f‖_[p] = n • ‖f‖_[p] := by - simp [dLpNorm, nnLpNorm_nsmul] +lemma dLpNorm_nsmul [NormedSpace ℝ E] (n : ℕ) (f : α → E) (p : ℝ≥0∞) : + ‖n • f‖_[p] = n • ‖f‖_[p] := by simp [dLpNorm, nnLpNorm_nsmul] variable [NormedSpace ℝ 𝕜]