Bohr sets

structure BohrSet (G : Type u_1) [Group G] : Type (max 1 u_1)

A Bohr set B on a group G is a finite set of unitary representations 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 {x | ∀ ψ ∈ B.frequencies, |arg (ψ x)| ≤ B.width ψ}.

Note that this set does not uniquely determine B (in particular, it does not uniquely determine either B.frequencies or B.width).

• frequencies : Finset (UnitaryDual ℂ G)
• ewidth : UnitaryDual ℂ G → ENNReal

  The width of a Bohr set at a frequency. Note that this width corresponds to chord-length.

• mem_frequencies (ψ : UnitaryDual ℂ G) : ψ ∈ self.frequencies ↔ self.ewidth ψ < ⊤

theorem BohrSet.ext_iff {G : Type u_1} {inst✝ : Group G} {x y : BohrSet G} : x = y ↔ x.frequencies = y.frequencies ∧ x.ewidth = y.ewidth

theorem BohrSet.ext {G : Type u_1} {inst✝ : Group G} {x y : BohrSet G} (frequencies : x.frequencies = y.frequencies) (ewidth : x.ewidth = y.ewidth) : x = y

def BohrSet.width {G : Type u_1} [Group G] (B : BohrSet G) (ψ : UnitaryDual ℂ G) : NNReal

Equations

• B.width ψ = (B.ewidth ψ).toNNReal

theorem BohrSet.coe_width {G : Type u_1} [Group G] {B : BohrSet G} {ψ : UnitaryDual ℂ G} (hψ : ψ ∈ B.frequencies) : ↑(B.width ψ) = B.ewidth ψ

theorem BohrSet.ewidth_eq_top_iff {G : Type u_1} [Group G] {B : BohrSet G} {ψ : UnitaryDual ℂ G} : ψ ∉ B.frequencies ↔ B.ewidth ψ = ⊤

theorem BohrSet.ewidth_eq_top_of_not_mem_frequencies {G : Type u_1} [Group G] {B : BohrSet G} {ψ : UnitaryDual ℂ G} : ψ ∉ B.frequencies → B.ewidth ψ = ⊤

Alias of the forward direction of BohrSet.ewidth_eq_top_iff.

theorem BohrSet.width_eq_zero_of_not_mem_frequencies {G : Type u_1} [Group G] {B : BohrSet G} {ψ : UnitaryDual ℂ G} (hψ : ψ ∉ B.frequencies) : B.width ψ = 0

theorem BohrSet.ewidth_injective {G : Type u_1} [Group G] : Function.Injective ewidth

noncomputable def BohrSet.ofEwidth {G : Type u_1} [Group G] [Finite G] (ewidth : UnitaryDual ℂ G → ENNReal) : BohrSet G

Construct a Bohr set on a finite group given an extended width function.

Equations

• BohrSet.ofEwidth ewidth = { frequencies := {ψ : UnitaryDual ℂ G | ewidth ψ < ⊤}, ewidth := ewidth, mem_frequencies := ⋯ }

noncomputable def BohrSet.ofWidth {G : Type u_1} [Group G] (width : UnitaryDual ℂ G → NNReal) (freq : Finset (UnitaryDual ℂ G)) : BohrSet G

Construct a Bohr set on a finite group given a width function and a frequency set.

Equations

• BohrSet.ofWidth width freq = { frequencies := freq, ewidth := fun (ψ : UnitaryDual ℂ G) => if ψ ∈ freq then ↑(width ψ) else ⊤, mem_frequencies := ⋯ }

theorem BohrSet.ext_width {G : Type u_1} [Group G] {B B' : BohrSet G} (freq : B.frequencies = B'.frequencies) (width : ∀ ψ ∈ B.frequencies, B.width ψ = B'.width ψ) : B = B'

theorem BohrSet.ext_width_iff {G : Type u_1} [Group G] {B B' : BohrSet G} : B = B' ↔ B.frequencies = B'.frequencies ∧ ∀ ψ ∈ B.frequencies, B.width ψ = B'.width ψ

Coercion, membership

def BohrSet.chordSet {G : Type u_1} [Group G] (B : BohrSet G) : Set G

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.

Equations

• ↑B = {x : G | ∀ (ψ : UnitaryDual ℂ G), ↑‖1 - ↑↑(ψ.ρ x)‖₊ ≤ B.ewidth ψ}

@[reducible, inline]

abbrev BohrSet.Elem {G : Type u_1} [Group G] (B : BohrSet G) : Type u_1

Given the Bohr set B, B.Elem is the Type of elements of B.

Equations

• ↑B = ↑↑B

@[implicit_reducible]

instance BohrSet.instCoe {G : Type u_1} [Group G] : Coe (BohrSet G) (Set G)

Equations

• BohrSet.instCoe = { coe := BohrSet.chordSet }

@[implicit_reducible]

instance BohrSet.instCoeSort {G : Type u_1} [Group G] : CoeSort (BohrSet G) (Type u_1)

Equations

• BohrSet.instCoeSort = { coe := BohrSet.Elem }

theorem BohrSet.mem_chordSet_iff_nnnorm_ewidth {G : Type u_1} [Group G] {B : BohrSet G} {x : G} : x ∈ ↑B ↔ ∀ (ψ : UnitaryDual ℂ G), ↑‖1 - ↑↑(ψ.ρ x)‖₊ ≤ B.ewidth ψ

theorem BohrSet.mem_chordSet_iff_nnnorm_width {G : Type u_1} [Group G] {B : BohrSet G} {x : G} : x ∈ ↑B ↔ ∀ ⦃ψ : UnitaryDual ℂ G⦄, ψ ∈ B.frequencies → ‖1 - ↑↑(ψ.ρ x)‖₊ ≤ B.width ψ

theorem BohrSet.mem_chordSet_iff_norm_width {G : Type u_1} [Group G] {B : BohrSet G} {x : G} : x ∈ ↑B ↔ ∀ ⦃ψ : UnitaryDual ℂ G⦄, ψ ∈ B.frequencies → ‖1 - ↑↑(ψ.ρ x)‖ ≤ ↑(B.width ψ)

@[simp]

theorem BohrSet.coeSort_coe {G : Type u_1} [Group G] (B : BohrSet G) : ↑↑B = ↑B

@[simp]

theorem BohrSet.one_mem_chordSet {G : Type u_1} [Group G] {B : BohrSet G} : 1 ∈ ↑B

@[simp]

theorem BohrSet.inv_mem_chordSet {G : Type u_1} [Group G] {B : BohrSet G} {x : G} : x⁻¹ ∈ ↑B ↔ x ∈ ↑B

@[simp]

theorem BohrSet.inv_chordSet {G : Type u_1} [Group G] {B : BohrSet G} : (↑B)⁻¹ = ↑B

@[simp]

theorem BohrSet.conj_mem_chordSet {G : Type u_1} [Group G] {B : BohrSet G} {x y : G} : y * x * y⁻¹ ∈ ↑B ↔ x ∈ ↑B

Lattice structure

@[implicit_reducible]

noncomputable instance BohrSet.instMax {G : Type u_1} [Group G] : Max (BohrSet G)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance BohrSet.instMin {G : Type u_1} [Group G] : Min (BohrSet G)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance BohrSet.instBotOfFinite {G : Type u_1} [Group G] [Finite G] : Bot (BohrSet G)

Equations

• BohrSet.instBotOfFinite = { bot := { frequencies := Finset.univ, ewidth := 0, mem_frequencies := ⋯ } }

@[implicit_reducible]

noncomputable instance BohrSet.instTop {G : Type u_1} [Group G] : Top (BohrSet G)

Equations

• BohrSet.instTop = { top := { frequencies := ∅, ewidth := ⊤, mem_frequencies := ⋯ } }

@[implicit_reducible]

instance BohrSet.instPreorder {G : Type u_1} [Group G] : Preorder (BohrSet G)

Equations

• BohrSet.instPreorder = Preorder.lift BohrSet.ewidth

@[implicit_reducible]

noncomputable instance BohrSet.instDistribLattice {G : Type u_1} [Group G] : DistribLattice (BohrSet G)

Equations

• BohrSet.instDistribLattice = Function.Injective.distribLattice BohrSet.ewidth ⋯ ⋯ ⋯ ⋯ ⋯

theorem BohrSet.le_iff_ewidth {G : Type u_1} [Group G] {B₁ B₂ : BohrSet G} : B₁ ≤ B₂ ↔ ∀ ⦃ψ : UnitaryDual ℂ G⦄, B₁.ewidth ψ ≤ B₂.ewidth ψ

theorem BohrSet.frequencies_anti {G : Type u_1} [Group G] {B₁ B₂ : BohrSet G} (h : B₁ ≤ B₂) : B₂.frequencies ⊆ B₁.frequencies

theorem BohrSet.frequencies_antitone {G : Type u_1} [Group G] : Antitone frequencies

theorem BohrSet.le_iff_width {G : Type u_1} [Group G] {B₁ B₂ : BohrSet G} : B₁ ≤ B₂ ↔ B₂.frequencies ⊆ B₁.frequencies ∧ ∀ ⦃ψ : UnitaryDual ℂ G⦄, ψ ∈ B₂.frequencies → B₁.width ψ ≤ B₂.width ψ

theorem BohrSet.width_le_width {G : Type u_1} [Group G] {ψ : UnitaryDual ℂ G} {B₁ B₂ : BohrSet G} (h : B₁ ≤ B₂) (hψ : ψ ∈ B₂.frequencies) : B₁.width ψ ≤ B₂.width ψ

@[implicit_reducible]

noncomputable instance BohrSet.instOrderTop {G : Type u_1} [Group G] : OrderTop (BohrSet G)

Equations

• BohrSet.instOrderTop = OrderTop.lift BohrSet.ewidth ⋯ ⋯

@[implicit_reducible]

noncomputable instance BohrSet.instSupSetOfFinite {G : Type u_1} [Group G] [Finite G] : SupSet (BohrSet G)

Equations

• One or more equations did not get rendered due to their size.

theorem BohrSet.iInf_lt_top {α : Type u_2} {β : Type u_3} [CompleteLattice β] {S : Set α} {f : α → β} : ⨅ i ∈ S, f i < ⊤ ↔ ∃ i ∈ S, f i < ⊤

@[implicit_reducible]

noncomputable instance BohrSet.instInfSetOfFinite {G : Type u_1} [Group G] [Finite G] : InfSet (BohrSet G)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BohrSet.minimalAxioms {G : Type u_1} [Group G] [Finite G] : CompletelyDistribLattice.MinimalAxioms (BohrSet G)

Equations

• BohrSet.minimalAxioms = Function.Injective.completelyDistribLatticeMinimalAxioms CompletelyDistribLattice.MinimalAxioms.of BohrSet.ewidth ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

noncomputable instance BohrSet.instCompletelyDistribLatticeOfFinite {G : Type u_1} [Group G] [Finite G] : CompletelyDistribLattice (BohrSet G)

Equations

• BohrSet.instCompletelyDistribLatticeOfFinite = CompletelyDistribLattice.ofMinimalAxioms BohrSet.minimalAxioms

Width, frequencies, rank

def BohrSet.cardRank {G : Type u_1} [Group G] (B : BohrSet G) : ℕ

The cardinality rank of a Bohr set is its number of frequencies.

Equations

• B.cardRank = B.frequencies.card

@[simp]

theorem BohrSet.card_frequencies {G : Type u_1} [Group G] (B : BohrSet G) : B.frequencies.card = B.cardRank

noncomputable def BohrSet.dimRank {G : Type u_1} [Group G] (B : BohrSet G) : ℕ

The dimension rank of a Bohr set is the sum of the dimensions of its frequencies.

Equations

• B.dimRank = ∑ ψ ∈ B.frequencies, Module.finrank ℂ ψ.E

noncomputable def BohrSet.dimSqRank {G : Type u_1} [Group G] (B : BohrSet G) : ℕ

The squared dimension rank of a Bohr set is the sum of the squares of the dimensions of its frequencies.

Equations

• B.dimSqRank = ∑ ψ ∈ B.frequencies, Module.finrank ℂ ψ.E ^ 2

theorem BohrSet.cardRank_le_dimRank {G : Type u_1} [Group G] {B : BohrSet G} : B.cardRank ≤ B.dimRank

Dilation

theorem BohrSet.nnreal_smul_lt_top {x : NNReal} {y : ENNReal} (hy : y < ⊤) : x • y < ⊤

theorem BohrSet.nnreal_smul_lt_top_iff {x : NNReal} {y : ENNReal} (hx : x ≠ 0) : x • y < ⊤ ↔ y < ⊤

theorem BohrSet.nnreal_smul_ne_top {x : NNReal} {y : ENNReal} (hy : y ≠ ⊤) : x • y ≠ ⊤

theorem BohrSet.nnreal_smul_ne_top_iff {x : NNReal} {y : ENNReal} (hx : x ≠ 0) : x • y ≠ ⊤ ↔ y ≠ ⊤

@[implicit_reducible]

noncomputable instance BohrSet.instSMul {G : Type u_1} [Group G] : SMul ℝ (BohrSet G)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BohrSet.frequencies_smul {G : Type u_1} [Group G] (ρ : ℝ) (B : BohrSet G) : (ρ • B).frequencies = B.frequencies

@[simp]

theorem BohrSet.cardRank_smul {G : Type u_1} [Group G] (ρ : ℝ) (B : BohrSet G) : (ρ • B).cardRank = B.cardRank

@[simp]

theorem BohrSet.dimRank_smul {G : Type u_1} [Group G] (ρ : ℝ) (B : BohrSet G) : (ρ • B).dimRank = B.dimRank

@[simp]

theorem BohrSet.ewidth_smul {G : Type u_1} [Group G] (ρ : ℝ) (B : BohrSet G) (ψ : UnitaryDual ℂ G) : (ρ • B).ewidth ψ = if ψ ∈ B.frequencies then ↑(Real.nnabs ρ) * B.ewidth ψ else ⊤

@[simp]

theorem BohrSet.width_smul_apply {G : Type u_1} [Group G] (ρ : ℝ) (B : BohrSet G) (ψ : UnitaryDual ℂ G) : (ρ • B).width ψ = Real.nnabs ρ * B.width ψ

theorem BohrSet.width_smul {G : Type u_1} [Group G] (ρ : ℝ) (B : BohrSet G) : (ρ • B).width = Real.nnabs ρ • B.width

@[implicit_reducible]

noncomputable instance BohrSet.instMulAction {G : Type u_1} [Group G] : MulAction ℝ (BohrSet G)

Equations

• BohrSet.instMulAction = { toSMul := BohrSet.instSMul, mul_smul := ⋯, one_smul := ⋯ }

theorem BohrSet.eq_singleton_one_of_ewidth_eq_zero {G : Type u_1} [Group G] {B : BohrSet G} (h : B.ewidth = 0) : ↑B = {1}

theorem BohrSet.chordSet_eq_top_of_two_le_width {G : Type u_1} [Group G] {B : BohrSet G} (h : ∀ (ψ : UnitaryDual ℂ G), 2 ≤ B.width ψ) : ↑B = Set.univ

theorem BohrSet.chordSet_mono {G : Type u_1} [Group G] {B₁ B₂ : BohrSet G} (h : B₁ ≤ B₂) : ↑B₁ ⊆ ↑B₂

theorem BohrSet.chordSet_monotone {G : Type u_1} [Group G] : Monotone chordSet

theorem BohrSet.chordSet_mul_chordSet_subset {G : Type u_1} [Group G] {B₁ B₂ B₃ : BohrSet G} (h : B₁.ewidth + B₂.ewidth ≤ B₃.ewidth) : ↑B₁ * ↑B₂ ⊆ ↑B₃

theorem BohrSet.chordSet_smul_add_chordSet_smul_subset {G : Type u_1} [Group G] {B : BohrSet G} {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 ≤ ρ₁) (hρ₂ : 0 ≤ ρ₂) : ↑(ρ₁ • B) * ↑(ρ₂ • B) ⊆ ↑((ρ₁ + ρ₂) • B)

@[simp]

theorem BohrSet.dimRank_eq_cardRank {G : Type u_1} [CommGroup G] (B : BohrSet G) : B.dimRank = B.cardRank

@[simp]

theorem BohrSet.dimSqRank_eq_cardRank {G : Type u_1} [CommGroup G] (B : BohrSet G) : B.dimSqRank = B.cardRank