From 2f2fd22f03a68da70d41b67d9917dd01f94b3725 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Fri, 30 Aug 2024 09:54:33 +0000 Subject: [PATCH] some arc sets --- LeanAPAP/Prereqs/Bohr/Basic.lean | 311 ++++++++++++++++++------------- 1 file changed, 186 insertions(+), 125 deletions(-) diff --git a/LeanAPAP/Prereqs/Bohr/Basic.lean b/LeanAPAP/Prereqs/Bohr/Basic.lean index 57234cc3cf..63fed1416f 100644 --- a/LeanAPAP/Prereqs/Bohr/Basic.lean +++ b/LeanAPAP/Prereqs/Bohr/Basic.lean @@ -1,18 +1,9 @@ -<<<<<<< HEAD import Mathlib.Analysis.Complex.Basic import LeanAPAP.Prereqs.AddChar.PontryaginDuality +import LeanAPAP.Prereqs.Function.Translate open AddChar Function open scoped NNReal ENNReal -======= -import LeanAPAP.Mathlib.Analysis.Normed.Field.Basic -import LeanAPAP.Mathlib.Data.ENNReal.Operations -import LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Basic -import LeanAPAP.Prereqs.AddChar.PontryaginDuality - -open AddChar Function -open scoped NNReal ENNReal Pointwise ->>>>>>> c88269882e68b9316c3a26cc19a33bee405c07c3 /-- 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 @@ -27,23 +18,20 @@ determine either `B.frequencies` or `B.width`). -/ @[ext] structure BohrSet (G : Type*) [AddCommGroup G] where frequencies : Finset (AddChar G ℂ) - /-- The width of a Bohr set at a frequency. - - Note that this width corresponds to chord-length under `BohrSet.toSet`, which is registered as the - coercion `BohrSet G → Set G`. For arc-length, use `BohrSet.arcSet` instead. -/ + /-- The width of a Bohr set at a frequency. Note that this width corresponds to chord-length. -/ ewidth : AddChar G ℂ → ℝ≥0∞ mem_frequencies : ∀ ψ, ψ ∈ frequencies ↔ ewidth ψ < ⊤ +attribute [-simp] Complex.norm_eq_abs -- just to make my life easier namespace BohrSet -variable {G : Type*} [AddCommGroup G] {B B₁ B₂ : BohrSet G} {ψ : AddChar G ℂ} {x : G} +variable {G : Type*} [AddCommGroup G] {B : BohrSet G} {ψ : AddChar G ℂ} {x : G} - /-- The width of a Bohr set at a frequency. Note that this width corresponds to chord-length. -/ def width (B : BohrSet G) (ψ : AddChar G ℂ) : ℝ≥0 := (B.ewidth ψ).toNNReal - lemma width_def : B.width ψ = (B.ewidth ψ).toNNReal := rfl -lemma coe_width (hψ : ψ ∈ B.frequencies) : B.width ψ = B.ewidth ψ := - ENNReal.coe_toNNReal <| by rwa [← lt_top_iff_ne_top, ← B.mem_frequencies] +lemma coe_width (hψ : ψ ∈ B.frequencies) : B.width ψ = B.ewidth ψ := by + refine ENNReal.coe_toNNReal ?_ + rwa [←lt_top_iff_ne_top, ←B.mem_frequencies] lemma ewidth_eq_top_iff : ψ ∉ B.frequencies ↔ B.ewidth ψ = ⊤ := by simp [B.mem_frequencies] @@ -53,21 +41,24 @@ alias ⟨ewidth_eq_top_of_not_mem_frequencies, _⟩ := ewidth_eq_top_iff lemma width_eq_zero_of_not_mem_frequencies (hψ : ψ ∉ B.frequencies) : B.width ψ = 0 := by rw [width_def, ewidth_eq_top_of_not_mem_frequencies hψ, ENNReal.top_toNNReal] -lemma ewidth_injective : Injective (BohrSet.ewidth (G := G)) := - fun B₁ B₂ h ↦ by ext <;> simp [B₁.mem_frequencies, B₂.mem_frequencies, h] +lemma ewidth_injective : Function.Injective (BohrSet.ewidth (G := G)) := by + intro B₁ B₂ h + ext ψ + case ewidth => rw [h] + case frequencies => rw [B₁.mem_frequencies, B₂.mem_frequencies, h] /-- Construct a Bohr set on a finite group given an extended width function. -/ -noncomputable def ofEWidth [Finite G] (ewidth : AddChar G ℂ → ℝ≥0∞) : BohrSet G where - frequencies := {ψ | ewidth ψ < ⊤} - ewidth := ewidth - mem_frequencies := fun ψ => by simp +noncomputable def ofEwidth [Finite G] (ewidth : AddChar G ℂ → ℝ≥0∞) : BohrSet G := + { frequencies := {ψ | ewidth ψ < ⊤}, + ewidth := ewidth, + mem_frequencies := fun ψ => by simp } /-- Construct a Bohr set on a finite group given a width function and a frequency set. -/ noncomputable def ofWidth (width : AddChar G ℂ → ℝ≥0) (freq : Finset (AddChar G ℂ)) : - BohrSet G where - frequencies := freq - ewidth ψ := if ψ ∈ freq then width ψ else ⊤ - mem_frequencies := fun ψ => by simp [lt_top_iff_ne_top] + BohrSet G := + { frequencies := freq, + ewidth := fun ψ => if ψ ∈ freq then width ψ else ⊤ , + mem_frequencies := fun ψ => by simp [lt_top_iff_ne_top] } @[ext] lemma ext_width {B B' : BohrSet G} (freq : B.frequencies = B'.frequencies) @@ -86,31 +77,47 @@ lemma ext_width {B B' : BohrSet G} (freq : B.frequencies = B'.frequencies) /-! ### Coercion, membership -/ -instance instMem : Membership G (BohrSet G) where - mem x B := ∀ ⦃ψ⦄, ψ ∈ B.frequencies → ‖1 - ψ x‖₊ ≤ B.width ψ +-- instance instMem : Membership G (BohrSet G) := +-- ⟨fun x B ↦ ∀ ψ, ‖1 - ψ x‖₊ ≤ B.ewidth ψ⟩ /-- The set corresponding to a Bohr set `B` is `{x | ∀ ψ ∈ B.frequencies, ‖1 - ψ x‖ ≤ B.width ψ}`. This is the *chord-length* convention. The arc-length convention would instead be `{x | ∀ ψ ∈ B.frequencies, |arg (ψ x)| ≤ B.width ψ}`. Note that this set **does not** uniquely determine `B`. -/ -@[coe] def toSet (B : BohrSet G) : Set G := {x | x ∈ B} +@[coe] def chordSet (B : BohrSet G) : Set G := {x | ∀ ψ, ‖1 - ψ x‖₊ ≤ B.ewidth ψ} /-- Given the Bohr set `B`, `B.Elem` is the `Type` of elements of `B`. -/ -@[coe, reducible] def Elem (B : BohrSet G) : Type _ := {x // x ∈ B} +@[coe, reducible] def Elem (B : BohrSet G) : Type _ := B.chordSet -instance instCoe : Coe (BohrSet G) (Set G) := ⟨toSet⟩ +instance instCoe : Coe (BohrSet G) (Set G) := ⟨chordSet⟩ instance instCoeSort : CoeSort (BohrSet G) (Type _) := ⟨Elem⟩ -lemma coe_def (B : BohrSet G) : B = {x | ∀ ⦃ψ⦄, ψ ∈ B.frequencies → ‖1 - ψ x‖₊ ≤ B.width ψ} := rfl -lemma mem_iff_nnnorm_width : x ∈ B ↔ ∀ ⦃ψ⦄, ψ ∈ B.frequencies → ‖1 - ψ x‖₊ ≤ B.width ψ := Iff.rfl -lemma mem_iff_norm_width : x ∈ B ↔ ∀ ⦃ψ⦄, ψ ∈ B.frequencies → ‖1 - ψ x‖ ≤ B.width ψ := Iff.rfl +lemma mem_chordSet_iff_nnnorm_ewidth : x ∈ B.chordSet ↔ ∀ ψ, ‖1 - ψ x‖₊ ≤ B.ewidth ψ := Iff.rfl + +lemma mem_chordSet_iff_nnnorm_width : + x ∈ B.chordSet ↔ ∀ ⦃ψ⦄, ψ ∈ B.frequencies → ‖1 - ψ x‖₊ ≤ B.width ψ := by + refine forall_congr' fun ψ => ?_ + constructor + case mpr => + intro h + rcases eq_top_or_lt_top (B.ewidth ψ) with h₁ | h₁ + case inl => simp [h₁] + case inr => + have : ψ ∈ B.frequencies := by simp [mem_frequencies, h₁] + specialize h this + rwa [←ENNReal.coe_le_coe, coe_width this] at h + case mp => + intro h₁ h₂ + rwa [←ENNReal.coe_le_coe, coe_width h₂] + +lemma mem_chordSet_iff_norm_width : x ∈ B.chordSet ↔ ∀ ⦃ψ⦄, ψ ∈ B.frequencies → ‖1 - ψ x‖ ≤ B.width ψ := + mem_chordSet_iff_nnnorm_width -@[simp, norm_cast] lemma mem_coe : x ∈ (B : Set G) ↔ x ∈ B := Iff.rfl @[simp, norm_cast] lemma coeSort_coe (B : BohrSet G) : ↥(B : Set G) = B := rfl -@[simp] lemma zero_mem : 0 ∈ B := by simp [mem_iff_nnnorm_width] -@[simp] lemma neg_mem [Finite G] : -x ∈ B ↔ x ∈ B := +@[simp] lemma zero_mem : 0 ∈ B.chordSet := by simp [mem_chordSet_iff_nnnorm_width] +@[simp] lemma neg_mem [Finite G] : -x ∈ B.chordSet ↔ x ∈ B.chordSet := forall₂_congr fun ψ hψ ↦ by sorry -- rw [Iff.comm, ← RCLike.nnnorm_conj, map_sub, map_one, map_neg_eq_conj] @@ -129,65 +136,37 @@ noncomputable instance : Inf (BohrSet G) where mem_frequencies := fun ψ => by simp [mem_frequencies] } noncomputable instance [Finite G] : Bot (BohrSet G) where - bot.frequencies := ⊤ - bot.ewidth := 0 - bot.mem_frequencies := by simp + bot := + { frequencies := ⊤, + ewidth := 0, + mem_frequencies := by simp } noncomputable instance : Top (BohrSet G) where - top.frequencies := ⊥ - top.ewidth := ⊤ - top.mem_frequencies := by simp - -@[simp] lemma frequencies_top : (⊤ : BohrSet G).frequencies = ∅ := rfl -@[simp] lemma frequencies_bot [Finite G] : (⊥ : BohrSet G).frequencies = .univ := rfl - -@[simp] lemma frequencies_sup (B₁ B₂ : BohrSet G) : - (B₁ ⊔ B₂).frequencies = B₁.frequencies ∩ B₂.frequencies := rfl - -@[simp] lemma frequencies_inf (B₁ B₂ : BohrSet G) : - (B₁ ⊓ B₂).frequencies = B₁.frequencies ∪ B₂.frequencies := rfl - -@[simp] lemma ewidth_top_apply (ψ : AddChar G ℂ) : (⊤ : BohrSet G).ewidth ψ = ∞ := rfl -@[simp] lemma ewidth_bot_apply [Finite G] (ψ : AddChar G ℂ) : (⊥ : BohrSet G).ewidth ψ = 0 := rfl -@[simp] lemma ewidth_sup_apply (B₁ B₂ : BohrSet G) (ψ : AddChar G ℂ) : - (B₁ ⊔ B₂).ewidth ψ = B₁.ewidth ψ ⊔ B₂.ewidth ψ := rfl -@[simp] lemma ewidth_inf_apply (B₁ B₂ : BohrSet G) (ψ : AddChar G ℂ) : - (B₁ ⊓ B₂).ewidth ψ = B₁.ewidth ψ ⊓ B₂.ewidth ψ := rfl - -@[simp] lemma width_top_apply (ψ : AddChar G ℂ) : (⊤ : BohrSet G).width ψ = 0 := rfl -@[simp] lemma width_bot_apply [Finite G] (ψ : AddChar G ℂ) : (⊥ : BohrSet G).width ψ = 0 := rfl -@[simp] lemma width_sup_apply (h₁ : ψ ∈ B₁.frequencies) (h₂ : B₂.frequencies) : - (B₁ ⊔ B₂).width ψ = B₁.width ψ ⊔ B₂.width ψ := sorry -@[simp] lemma width_inf_apply (h₁ : ψ ∈ B₁.frequencies) (h₂ : B₂.frequencies) : - (B₁ ⊓ B₂).width ψ = B₁.width ψ ⊓ B₂.width ψ := sorry - -lemma ewidth_top : (⊤ : BohrSet G).ewidth = ⊤ := rfl -lemma ewidth_bot [Finite G] : (⊥ : BohrSet G).ewidth = 0 := rfl -lemma ewidth_sup (B₁ B₂ : BohrSet G) : (B₁ ⊔ B₂).ewidth = B₁.ewidth ⊔ B₂.ewidth := rfl -lemma ewidth_inf (B₁ B₂ : BohrSet G) : (B₁ ⊓ B₂).ewidth = B₁.ewidth ⊓ B₂.ewidth := rfl - -lemma width_top : (⊤ : BohrSet G).width = 0 := rfl -lemma width_bot [Finite G] : (⊥ : BohrSet G).width = 0 := rfl -lemma width_sup (h₁ : ψ ∈ B₁.frequencies) (h₂ : B₂.frequencies) : - (B₁ ⊔ B₂).width = B₁.width ⊔ B₂.width := sorry -lemma width_inf (h₁ : ψ ∈ B₁.frequencies) (h₂ : B₂.frequencies) : - (B₁ ⊓ B₂).width = B₁.width ⊓ B₂.width := sorry + top := + { frequencies := ⊥, + ewidth := ⊤, + mem_frequencies := by simp } noncomputable instance : DistribLattice (BohrSet G) := - ewidth_injective.distribLattice BohrSet.ewidth ewidth_sup ewidth_inf - -noncomputable instance : OrderTop (BohrSet G) := OrderTop.lift BohrSet.ewidth (fun _ _ h ↦ h) rfl + Function.Injective.distribLattice BohrSet.ewidth + ewidth_injective + (fun _ _ => rfl) + (fun _ _ => rfl) -lemma le_iff_ewidth : B₁ ≤ B₂ ↔ ∀ ⦃ψ⦄, B₁.ewidth ψ ≤ B₂.ewidth ψ := Iff.rfl +lemma le_iff_ewidth {B₁ B₂ : BohrSet G} : B₁ ≤ B₂ ↔ ∀ ⦃ψ⦄, B₁.ewidth ψ ≤ B₂.ewidth ψ := Iff.rfl -@[gcongr] lemma frequencies_anti (h : B₁ ≤ B₂) : B₂.frequencies ⊆ B₁.frequencies := - fun ψ ↦ by simpa only [mem_frequencies] using (h ψ).trans_lt +@[gcongr] +lemma frequencies_anti {B₁ B₂ : BohrSet G} (h : B₁ ≤ B₂) : + B₂.frequencies ⊆ B₁.frequencies := by + intro ψ hψ + simp only [mem_frequencies] at hψ ⊢ + exact (h ψ).trans_lt hψ -lemma frequencies_antitone : Antitone (frequencies : BohrSet G → _) := fun _ _ ↦ frequencies_anti +lemma frequencies_antitone : Antitone (frequencies : BohrSet G → _) := + fun _ _ => frequencies_anti -lemma le_iff_width : - B₁ ≤ B₂ ↔ - B₂.frequencies ⊆ B₁.frequencies ∧ ∀ ⦃ψ⦄, ψ ∈ B₂.frequencies → B₁.width ψ ≤ B₂.width ψ := by +lemma le_iff_width {B₁ B₂ : BohrSet G} : B₁ ≤ B₂ ↔ + B₂.frequencies ⊆ B₁.frequencies ∧ ∀ ⦃ψ⦄, ψ ∈ B₂.frequencies → B₁.width ψ ≤ B₂.width ψ := by constructor case mp => intro h @@ -202,11 +181,15 @@ lemma le_iff_width : rw [←coe_width h', ←coe_width (h₁ h'), ENNReal.coe_le_coe] exact h₂ h' -@[gcongr] lemma ewidth_mono (h : B₁ ≤ B₂) : B₁.ewidth ψ ≤ B₂.ewidth ψ := h ψ - @[gcongr] -lemma width_mono (h : B₁ ≤ B₂) (hψ : ψ ∈ B₂.frequencies) : B₁.width ψ ≤ B₂.width ψ := - (le_iff_width.1 h).2 hψ +lemma width_le_width {B₁ B₂ : BohrSet G} (h : B₁ ≤ B₂) {ψ : AddChar G ℂ} (hψ : ψ ∈ B₂.frequencies) : + B₁.width ψ ≤ B₂.width ψ := by + rw [le_iff_width] at h + exact h.2 hψ + +noncomputable instance : OrderTop (BohrSet G) := OrderTop.lift BohrSet.ewidth (fun _ _ h => h) rfl + +example [Finite G] : Finite (AddChar G ℂ) := by infer_instance open scoped Classical in noncomputable instance [Finite G] : SupSet (BohrSet G) where @@ -215,6 +198,10 @@ noncomputable instance [Finite G] : SupSet (BohrSet G) where ewidth := fun ψ => ⨆ i ∈ B, ewidth i ψ mem_frequencies := fun ψ => by simp [mem_frequencies] } +lemma iInf_lt_top {α β : Type*} [CompleteLattice β] {S : Set α} {f : α → β}: + (⨅ i ∈ S, f i) < ⊤ ↔ ∃ i ∈ S, f i < ⊤ := by + simp [lt_top_iff_ne_top] + open scoped Classical in noncomputable instance [Finite G] : InfSet (BohrSet G) where sInf B := @@ -222,10 +209,20 @@ noncomputable instance [Finite G] : InfSet (BohrSet G) where ewidth := fun ψ => ⨅ i ∈ B, ewidth i ψ mem_frequencies := by simp [iInf_lt_top] } -noncomputable def minimalAxioms [Finite G] : CompletelyDistribLattice.MinimalAxioms (BohrSet G) := - ewidth_injective.completelyDistribLatticeMinimalAxioms .of BohrSet.ewidth ewidth_sup ewidth_inf - (fun B => by ext ψ; simp only [iSup_apply]; rfl) - (fun B => by ext ψ; simp only [iInf_apply]; rfl) +noncomputable def minimalAxioms [Finite G] : + CompletelyDistribLattice.MinimalAxioms (BohrSet G) := + Function.Injective.completelyDistribLatticeMinimalAxioms .of BohrSet.ewidth + ewidth_injective + (fun _ _ => rfl) + (fun _ _ => rfl) + (fun B => by + ext ψ + simp only [iSup_apply] + rfl) + (fun B => by + ext ψ + simp only [iInf_apply] + rfl) rfl rfl @@ -244,27 +241,55 @@ def rank (B : BohrSet G) : ℕ := B.frequencies.card section smul variable {ρ : ℝ} +lemma nnreal_smul_lt_top {x : ℝ≥0} {y : ℝ≥0∞} (hy : y < ⊤) : x • y < ⊤ := + ENNReal.mul_lt_top (by simp) hy + +lemma nnreal_smul_lt_top_iff {x : ℝ≥0} {y : ℝ≥0∞} (hx : x ≠ 0) : x • y < ⊤ ↔ y < ⊤ := by + constructor + case mpr => exact nnreal_smul_lt_top + case mp => + intro h + by_contra hy + simp only [top_le_iff, not_lt] at hy + simp [hy, ENNReal.smul_top, hx] at h + +lemma nnreal_smul_ne_top {x : ℝ≥0} {y : ℝ≥0∞} (hy : y ≠ ⊤) : x • y ≠ ⊤ := + ENNReal.mul_ne_top (by simp) hy + +lemma nnreal_smul_ne_top_iff {x : ℝ≥0} {y : ℝ≥0∞} (hx : x ≠ 0) : x • y ≠ ⊤ ↔ y ≠ ⊤ := by + constructor + case mpr => exact nnreal_smul_ne_top + case mp => + intro h + by_contra hy + simp [hy, ENNReal.smul_top, hx] at h + +open scoped Classical + noncomputable instance instSMul : SMul ℝ (BohrSet G) where smul ρ B := BohrSet.mk B.frequencies - (fun ψ => if ψ ∈ B.frequencies then Real.nnabs ρ * B.width ψ else ⊤) fun ψ => by - simp [lt_top_iff_ne_top, ←ENNReal.coe_mul] + (fun ψ => if ψ ∈ B.frequencies then Real.nnabs ρ * B.ewidth ψ else ⊤) fun ψ => by + simp only [lt_top_iff_ne_top, ite_ne_right_iff, Classical.not_imp, iff_self_and] + intro hψ + refine ENNReal.mul_ne_top (by simp) ?_ + rwa [←lt_top_iff_ne_top, ←mem_frequencies] @[simp] lemma frequencies_smul (ρ : ℝ) (B : BohrSet G) : (ρ • B).frequencies = B.frequencies := rfl @[simp] lemma rank_smul (ρ : ℝ) (B : BohrSet G) : (ρ • B).rank = B.rank := rfl @[simp] lemma ewidth_smul (ρ : ℝ) (B : BohrSet G) (ψ) : - (ρ • B).ewidth ψ = if ψ ∈ B.frequencies then (Real.nnabs ρ * B.width ψ : ℝ≥0∞) else ⊤ := - rfl + (ρ • B).ewidth ψ = if ψ ∈ B.frequencies then Real.nnabs ρ * B.ewidth ψ else ⊤ := rfl @[simp] lemma width_smul_apply (ρ : ℝ) (B : BohrSet G) (ψ) : (ρ • B).width ψ = Real.nnabs ρ * B.width ψ := by rw [width_def, ewidth_smul] split - case isTrue h => simp + case isTrue h => simp [←coe_width h] case isFalse h => simp [width_eq_zero_of_not_mem_frequencies h] lemma width_smul (ρ : ℝ) (B : BohrSet G) : (ρ • B).width = Real.nnabs ρ • B.width := by - ext ψ; simp [width_smul_apply] + ext ψ + simp [width_smul_apply] noncomputable instance instMulAction : MulAction ℝ (BohrSet G) where one_smul B := by ext <;> simp @@ -274,9 +299,9 @@ end smul -- Note it is not sufficient to say B.width = 0. lemma eq_zero_of_ewidth_eq_zero {B : BohrSet G} [Finite G] (h : B.ewidth = 0) : - (B : Set G) = {0} := by + B.chordSet = {0} := by rw [Set.eq_singleton_iff_unique_mem] - simp only [mem_coe, zero_mem, true_and, mem_iff_nnnorm_width, map_zero_eq_one, sub_self, + simp only [zero_mem, true_and, mem_chordSet_iff_nnnorm_width, map_zero_eq_one, sub_self, norm_zero, true_and, NNReal.zero_le_coe, implies_true, nnnorm_zero, zero_le] intro x hx by_contra! @@ -294,18 +319,17 @@ lemma eq_zero_of_ewidth_eq_zero {B : BohrSet G} [Finite G] (h : B.ewidth = 0) : NNReal.coe_injective (by simp) lemma eq_top_of_two_le_width {B : BohrSet G} [Finite G] (h : ∀ ψ, 2 ≤ B.width ψ) : - (B : Set G) = Set.univ := by - simp only [Set.eq_univ_iff_forall, mem_coe, mem_iff_nnnorm_width] + B.chordSet = Set.univ := by + simp only [Set.eq_univ_iff_forall, mem_chordSet_iff_nnnorm_width] intro i ψ _ calc ‖1 - ψ i‖₊ ≤ ‖(1 : ℂ)‖₊ + ‖ψ i‖₊ := nnnorm_sub_le _ _ _ = 2 := by norm_num _ ≤ B.width ψ := h _ -lemma toSet_mono {B₁ B₂ : BohrSet G} (h : B₁ ≤ B₂) : - B₁.toSet ⊆ B₂.toSet := fun _ hx _ hψ => - (hx (frequencies_anti h hψ)).trans (width_le_width h hψ) +@[gcongr] lemma chordSet_mono {B₁ B₂ : BohrSet G} (h : B₁ ≤ B₂) : B₁.chordSet ⊆ B₂.chordSet := + fun _ hx ψ => (hx ψ).trans (h ψ) -lemma toSet_monotone : Monotone (toSet : BohrSet G → Set G) := fun _ _ => toSet_mono +lemma chordSet_monotone : Monotone (chordSet : BohrSet G → Set G) := fun _ _ => chordSet_mono open Pointwise @@ -329,21 +353,58 @@ lemma nnnorm_one_sub_mul' {R : Type*} [SeminormedRing R] {a b c : R} (hb : ‖b ‖c - a * b‖₊ ≤ ‖1 - a‖₊ + ‖c - b‖₊ := norm_one_sub_mul' hb -lemma smul_add_smul_subset [Finite G] {B : BohrSet G} {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 ≤ ρ₁) (hρ₂ : 0 ≤ ρ₂) : - (ρ₁ • B).toSet + (ρ₂ • B).toSet ⊆ ((ρ₁ + ρ₂) • B).toSet := by +lemma add_subset_of_ewidth [Finite G] {B₁ B₂ B₃ : BohrSet G} + (h : B₁.ewidth + B₂.ewidth ≤ B₃.ewidth) : + B₁.chordSet + B₂.chordSet ⊆ B₃.chordSet := by intro x - simp only [Set.mem_add, mem_coe, mem_iff_norm_width, frequencies_smul, width_smul_apply, - NNReal.coe_mul, Real.coe_nnabs, forall_exists_index, and_imp] - rintro y h₁ z h₂ rfl ψ hψ - rw [AddChar.map_add_eq_mul] - refine (norm_one_sub_mul (by simp)).trans ?_ - simp only [abs_of_nonneg, add_nonneg, hρ₁, hρ₂] at h₁ h₂ ⊢ - linarith [h₁ hψ, h₂ hψ] + simp only [mem_chordSet_iff_nnnorm_ewidth, Set.mem_add, forall_exists_index, and_imp] + rintro x hx y hy rfl ψ + rw [map_add_eq_mul] + have : ‖1 - ψ x * ψ y‖₊ ≤ ‖1 - ψ x‖₊ + _ := nnnorm_one_sub_mul (by simp) + rw [←ENNReal.coe_le_coe, ENNReal.coe_add] at this + exact this.trans <| (h _).trans' <| add_le_add (hx _) (hy _) -variable {ρ : ℝ} +lemma smul_add_smul_subset [Finite G] {B : BohrSet G} {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 ≤ ρ₁) (hρ₂ : 0 ≤ ρ₂) : + (ρ₁ • B).chordSet + (ρ₂ • B).chordSet ⊆ ((ρ₁ + ρ₂) • B).chordSet := + add_subset_of_ewidth fun ψ => by + simp only [Pi.add_apply, ewidth_smul]; split <;> simp [add_nonneg, add_mul, *] -lemma le_card_smul (hρ₀ : 0 < ρ) (hρ₁ : ρ < 1) : - (ρ / 4) ^ B.rank * Nat.card B ≤ Nat.card ↥(ρ • B) := by +/- ### Arc Bohr sets -/ + +def arcSet : Set G := {x | ∀ ψ, ‖(ψ x).arg‖₊ ≤ B.ewidth ψ} + +lemma mem_arcSet_iff_nnnorm_ewidth : x ∈ B.arcSet ↔ ∀ ψ, ‖(ψ x).arg‖₊ ≤ B.ewidth ψ := Iff.rfl + +lemma mem_arcSet_iff_nnnorm_width : + x ∈ B.arcSet ↔ ∀ ⦃ψ⦄, ψ ∈ B.frequencies → ‖(ψ x).arg‖₊ ≤ B.width ψ := by + refine forall_congr' fun ψ => ?_ + constructor + case mpr => + intro h + rcases eq_top_or_lt_top (B.ewidth ψ) with h₁ | h₁ + case inl => simp [h₁] + case inr => + have : ψ ∈ B.frequencies := by simp [mem_frequencies, h₁] + specialize h this + rwa [←ENNReal.coe_le_coe, coe_width this] at h + case mp => + intro h₁ h₂ + rwa [←ENNReal.coe_le_coe, coe_width h₂] + +lemma mem_arcSet_iff_norm_width : + x ∈ B.arcSet ↔ ∀ ⦃ψ⦄, ψ ∈ B.frequencies → ‖(ψ x).arg‖ ≤ B.width ψ := + mem_arcSet_iff_nnnorm_width + +lemma arcSet_subset_chordSet : + B.arcSet ⊆ B.chordSet := fun x hx ψ => by + refine (hx ψ).trans' ?_ + simp only [ENNReal.coe_le_coe] sorry end BohrSet + +-- variable {ρ : ℝ} + +-- lemma le_card_smul (hρ₀ : 0 < ρ) (hρ₁ : ρ < 1) : +-- (ρ / 4) ^ B.rank * Nat.card B ≤ Nat.card ↥(ρ • B) := by +-- sorry