Skip to content

Commit

Permalink
start fixing almost periodicity
Browse files Browse the repository at this point in the history
  • Loading branch information
@YaelDillies
YaelDillies committed Aug 29, 2024
1 parent 96efe64 commit 0e42a93
Show file tree
Hide file tree
Showing 3 changed files with 107 additions and 95 deletions.
194 changes: 103 additions & 91 deletions LeanAPAP/Physics/AlmostPeriodicity.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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

Expand All @@ -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
Expand All @@ -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
Expand All @@ -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]
Expand All @@ -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) ≤
Expand All @@ -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) :
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ℝ 𝕜]

Expand Down
4 changes: 2 additions & 2 deletions LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ℝ 𝕜]

Expand Down

0 comments on commit 0e42a93

Please sign in to comment.