wip bohr sets

LeanAPAP/Prereqs/Bohr/Basic.lean

@@ -1,10 +1,12 @@
 import Mathlib.Analysis.Complex.Basic
+import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 
-open AddChar Complex Function
-open scoped NNReal
+open AddChar Function
+open scoped NNReal ENNReal
 
-/-- A *Bohr set* `B` on an additive group `G` is a set of characters of `G`, called the
-*frequencies*, along with a real number for each frequency `ψ`, called the *width of `B` at `ψ`*.
+/-- 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
+*width of `B` at `ψ`*.
 
 A Bohr set `B` is thought of as the set `{x | ∀ ψ ∈ B.frequencies, ‖1 - ψ x‖ ≤ B.width ψ}`. This is
 the *chord-length* convention. The arc-length convention would instead be
@@ -14,71 +16,335 @@ Note that this set **does not** uniquely determine `B` (in particular, it does n
 determine either `B.frequencies` or `B.width`). -/
 @[ext]
 structure BohrSet (G : Type*) [AddCommGroup G] where
-  /-- The set of frequencies of a Bohr set. -/
   frequencies : Finset (AddChar G ℂ)
   /-- The width of a Bohr set at a frequency. Note that this width corresponds to chord-length. -/
-  width : frequencies → ℝ≥0
+  ewidth : AddChar G ℂ → ℝ≥0∞
+  mem_frequencies : ∀ ψ, ψ ∈ frequencies ↔ ewidth ψ < ⊤
 
 namespace BohrSet
-variable {G : Type*} [AddCommGroup G] {B : BohrSet G} {x : G}
+variable {G : Type*} [AddCommGroup G] {B : BohrSet G} {ψ : AddChar G ℂ} {x : G}
+
+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 ψ := 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]
+
+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 : 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 :=
+  { 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 :=
+  { 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)
+    (width : ∀ ψ : AddChar G ℂ, ψ ∈ B.frequencies → B.width ψ = B'.width ψ) :
+    B = B' := by
+  ext
+  case frequencies => rw [freq]
+  case ewidth ψ =>
+    by_cases hψ : ψ ∈ B.frequencies
+    case pos =>
+      rw [←coe_width hψ, width _ hψ, coe_width]
+      rwa [←freq]
+    case neg =>
+      rw [ewidth_eq_top_of_not_mem_frequencies hψ, ewidth_eq_top_of_not_mem_frequencies]
+      rwa [←freq]
 
 /-! ### Coercion, membership -/
 
-instance instMem : Membership G (BohrSet G) := ⟨fun x B ↦ ∀ ψ, ‖1 - ψ.1 x‖ ≤ B.width ψ⟩
+instance instMem : Membership G (BohrSet G) :=
+  ⟨fun x B ↦ ∀ ⦃ψ⦄, ψ ∈ B.frequencies → ‖1 - ψ x‖₊ ≤ B.width ψ⟩
 
 /-- 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 | ∀ ψ, ‖1 - ψ.1 x‖ ≤ B.width ψ}
+@[coe] def toSet (B : BohrSet G) : Set G := {x | x ∈ B}
 
 /-- 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}
 
 instance instCoe : Coe (BohrSet G) (Set G) := ⟨toSet⟩
 instance instCoeSort : CoeSort (BohrSet G) (Type _) := ⟨Elem⟩
 
-lemma coe_def (B : BohrSet G) : B = {x | ∀ ψ, ‖1 - ψ.1 x‖ ≤ B.width ψ} := rfl
-lemma mem_def : x ∈ B ↔ ∀ ψ, ‖1 - ψ.1 x‖ ≤ B.width ψ := Iff.rfl
+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
 
 @[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_def]
+@[simp] lemma zero_mem : 0 ∈ B := by simp [mem_iff_nnnorm_width]
 @[simp] lemma neg_mem [Finite G] : -x ∈ B ↔ x ∈ B :=
-  forall_congr' fun ψ ↦ by rw [Iff.comm, ← RCLike.norm_conj, map_sub, map_one, map_neg_eq_conj]
+  forall₂_congr fun ψ hψ ↦ by sorry
+    -- rw [Iff.comm, ← RCLike.nnnorm_conj, map_sub, map_one, map_neg_eq_conj]
+
+/-! ### Lattice structure -/
+
+noncomputable instance : Sup (BohrSet G) where
+  sup B₁ B₂ :=
+    { frequencies := B₁.frequencies ∩ B₂.frequencies,
+      ewidth := fun ψ => B₁.ewidth ψ ⊔ B₂.ewidth ψ,
+      mem_frequencies := fun ψ => by simp [mem_frequencies] }
+
+noncomputable instance : Inf (BohrSet G) where
+  inf B₁ B₂ :=
+    { frequencies := B₁.frequencies ∪ B₂.frequencies,
+      ewidth := fun ψ => B₁.ewidth ψ ⊓ B₂.ewidth ψ,
+      mem_frequencies := fun ψ => by simp [mem_frequencies] }
+
+noncomputable instance [Finite G] : Bot (BohrSet G) where
+  bot :=
+    { frequencies := ⊤,
+      ewidth := 0,
+      mem_frequencies := by simp }
+
+noncomputable instance : Top (BohrSet G) where
+  top :=
+    { frequencies := ⊥,
+      ewidth := ⊤,
+      mem_frequencies := by simp }
+
+noncomputable instance : DistribLattice (BohrSet G) :=
+  Function.Injective.distribLattice BohrSet.ewidth
+    ewidth_injective
+    (fun _ _ => rfl)
+    (fun _ _ => rfl)
+
+lemma le_iff_ewidth {B₁ B₂ : BohrSet G} : B₁ ≤ B₂ ↔ ∀ ⦃ψ⦄, B₁.ewidth ψ ≤ B₂.ewidth ψ := Iff.rfl
+
+@[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 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
+    refine ⟨frequencies_anti h, fun ψ hψ => ?_⟩
+    rw [←ENNReal.coe_le_coe, coe_width hψ, coe_width (frequencies_anti h hψ)]
+    exact h ψ
+  case mpr =>
+    rintro ⟨h₁, h₂⟩ ψ
+    by_cases ψ ∈ B₂.frequencies
+    case neg h' => simp [ewidth_eq_top_of_not_mem_frequencies h']
+    case pos h' =>
+      rw [←coe_width h', ←coe_width (h₁ h'), ENNReal.coe_le_coe]
+      exact h₂ h'
+
+@[gcongr]
+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
+  sSup B :=
+    { frequencies := {ψ | ⨆ i ∈ B, i.ewidth ψ < ⊤},
+      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 :=
+    { frequencies := {ψ | ∃ i ∈ B, i.ewidth ψ < ⊤},
+      ewidth := fun ψ => ⨅ i ∈ B, ewidth i ψ
+      mem_frequencies := by simp [iInf_lt_top] }
+
+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
+
+noncomputable instance [Finite G] : CompletelyDistribLattice (BohrSet G) :=
+  .ofMinimalAxioms BohrSet.minimalAxioms
 
 /-! ### Width, frequencies, rank -/
 
-/-- The rank of a Bohr set is the number of characters which have width strictly less than `2`. -/
+/-- The rank of a Bohr set is the number of characters which have finite width. -/
 def rank (B : BohrSet G) : ℕ := B.frequencies.card
 
-lemma card_frequencies (B : BohrSet G) : B.frequencies.card = B.rank := rfl
+@[simp] lemma card_frequencies (B : BohrSet G) : B.frequencies.card = B.rank := rfl
 
 /-! ### Dilation -/
 
 section smul
 variable {ρ : ℝ}
 
-noncomputable instance instSMul : SMul ℝ (BohrSet G) where
-  smul ρ B := ⟨B.frequencies, fun ψ ↦ Real.nnabs ρ • B.width ψ⟩
+lemma nnreal_smul_lt_top {x : ℝ≥0} {y : ℝ≥0∞} (hy : y < ⊤) : x • y < ⊤ :=
+  ENNReal.mul_lt_top (by simp) hy.ne
+
+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 smul_def (ρ : ℝ) (B : BohrSet G) :
-    ρ • B = ⟨B.frequencies, fun ψ ↦ Real.nnabs ρ • B.width ψ⟩ := rfl
+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]
 
 @[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 width_smul (ρ : ℝ) (B : BohrSet G) (ψ : B.frequencies) :
-    (ρ • B).width ψ = Real.nnabs ρ • B.width ψ := rfl
+@[simp] lemma ewidth_smul (ρ : ℝ) (B : BohrSet G) (ψ) :
+    (ρ • B).ewidth ψ = if ψ ∈ B.frequencies then (Real.nnabs ρ * B.width ψ : ℝ≥0∞) 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 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]
 
 noncomputable instance instMulAction : MulAction ℝ (BohrSet G) where
-  one_smul B := by simp [smul_def]
-  mul_smul ρ φ B := by simp [smul_def, mul_smul, mul_assoc]
+  one_smul B := by ext <;> simp
+  mul_smul ρ φ B := by ext <;> simp [mul_assoc]
 
 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
+  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,
+    norm_zero, true_and, NNReal.zero_le_coe, implies_true, nnnorm_zero, zero_le]
+  intro x hx
+  by_contra!
+  rw [←AddChar.exists_apply_ne_zero] at this
+  obtain ⟨ψ, hψ⟩ := this
+  apply hψ
+  have hψ' : ψ ∈ B.frequencies := by simp [B.mem_frequencies, h]
+  specialize hx hψ'
+  rwa [B.width_def, h, Pi.zero_apply, ENNReal.zero_toNNReal, nonpos_iff_eq_zero, nnnorm_eq_zero,
+    sub_eq_zero, eq_comm] at hx
+
+@[simp] lemma AddChar.nnnorm_apply {α G : Type*}
+    [NormedDivisionRing α] [AddLeftCancelMonoid G] [Finite G] (ψ : AddChar G α)
+    (x : G) : ‖ψ x‖₊ = 1 :=
+  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]
+  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ψ)
+
+lemma toSet_monotone : Monotone (toSet : BohrSet G → Set G) := fun _ _ => toSet_mono
+
+open Pointwise
+
+lemma norm_one_sub_mul {R : Type*} [SeminormedRing R] {a b c : R} (ha : ‖a‖ ≤ 1) :
+    ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖ := by
+  calc ‖c - a * b‖ = ‖(c - a) + a * (1 - b)‖ := by noncomm_ring
+    _ ≤ ‖c - a‖ + ‖a * (1 - b)‖ := norm_add_le _ _
+    _ ≤ ‖c - a‖ + ‖a‖ * ‖1 - b‖ := add_le_add_left (norm_mul_le _ _) _
+    _ ≤ ‖c - a‖ + 1 * ‖1 - b‖ := by gcongr
+    _ = ‖c - a‖ + ‖1 - b‖ := by simp
+
+lemma norm_one_sub_mul' {R : Type*} [SeminormedRing R] {a b c : R} (hb : ‖b‖ ≤ 1) :
+    ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖ :=
+  (norm_one_sub_mul (R := Rᵐᵒᵖ) hb).trans_eq (add_comm _ _)
+
+lemma nnnorm_one_sub_mul {R : Type*} [SeminormedRing R] {a b c : R} (ha : ‖a‖₊ ≤ 1) :
+    ‖c - a * b‖₊ ≤ ‖c - a‖₊ + ‖1 - b‖₊ :=
+  norm_one_sub_mul ha
+
+lemma nnnorm_one_sub_mul' {R : Type*} [SeminormedRing R] {a b c : R} (hb : ‖b‖₊ ≤ 1) :
+    ‖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
+  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ψ]
+
 variable {ρ : ℝ}
 
 lemma le_card_smul (hρ₀ : 0 < ρ) (hρ₁ : ρ < 1) :