structure BohrSet (G : Type u_1) [AddCommGroup G] : Type u_1

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 {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 (AddChar G ℂ)
• ewidth : AddChar G ℂ → ENNReal

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

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

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

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

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

Equations

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

theorem BohrSet.width_def {G : Type u_1} [AddCommGroup G] {B : BohrSet G} {ψ : AddChar G ℂ} : B.width ψ = (B.ewidth ψ).toNNReal

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

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

theorem BohrSet.ewidth_eq_top_of_not_mem_frequencies {G : Type u_1} [AddCommGroup G] {B : BohrSet G} {ψ : AddChar 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} [AddCommGroup G] {B : BohrSet G} {ψ : AddChar G ℂ} (hψ : ψ ∉ B.frequencies) : B.width ψ = 0

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

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

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

Equations

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

noncomputable def BohrSet.ofWidth {G : Type u_1} [AddCommGroup G] (width : AddChar G ℂ → NNReal) (freq : Finset (AddChar 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 (ψ : AddChar G ℂ) => if ψ ∈ freq then ↑(width ψ) else ⊤, mem_frequencies := ⋯ }

theorem BohrSet.ext_width {G : Type u_1} [AddCommGroup 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} [AddCommGroup 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} [AddCommGroup 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 | ∀ (ψ : AddChar G ℂ), ↑‖1 - ψ x‖₊ ≤ B.ewidth ψ}

@[reducible]

def BohrSet.Elem {G : Type u_1} [AddCommGroup G] (B : BohrSet G) : Type u_1

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

Equations

• ↑B = ↑↑B

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

Equations

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

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

Equations

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

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

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

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

@[simp]

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

@[simp]

theorem BohrSet.zero_mem {G : Type u_1} [AddCommGroup G] {B : BohrSet G} : 0 ∈ ↑B

@[simp]

theorem BohrSet.neg_mem {G : Type u_1} [AddCommGroup G] {B : BohrSet G} {x : G} [Finite G] : -x ∈ ↑B ↔ x ∈ ↑B

Lattice structure

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

Equations

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

noncomputable instance BohrSet.instSupSetOfFinite {G : Type u_1} [AddCommGroup 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 < ⊤

noncomputable instance BohrSet.instInfSetOfFinite {G : Type u_1} [AddCommGroup 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} [AddCommGroup G] [Finite G] : CompletelyDistribLattice.MinimalAxioms (BohrSet G)

Equations

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

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

Equations

• BohrSet.instCompletelyDistribLatticeOfFinite = CompletelyDistribLattice.ofMinimalAxioms BohrSet.minimalAxioms

Width, frequencies, rank

def BohrSet.rank {G : Type u_1} [AddCommGroup G] (B : BohrSet G) : ℕ

The rank of a Bohr set is the number of characters which have finite width.

Equations

• B.rank = B.frequencies.card

@[simp]

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

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 ≠ ⊤

noncomputable instance BohrSet.instSMul {G : Type u_1} [AddCommGroup 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} [AddCommGroup G] (ρ : ℝ) (B : BohrSet G) : (ρ • B).frequencies = B.frequencies

@[simp]

theorem BohrSet.rank_smul {G : Type u_1} [AddCommGroup G] (ρ : ℝ) (B : BohrSet G) : (ρ • B).rank = B.rank

@[simp]

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

@[simp]

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

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

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

Equations

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

theorem BohrSet.eq_zero_of_ewidth_eq_zero {G : Type u_1} [AddCommGroup G] {B : BohrSet G} [Finite G] (h : B.ewidth = 0) : ↑B = {0}

@[simp]

theorem BohrSet.AddChar.nnnorm_apply {α : Type u_2} {G : Type u_3} [NormedDivisionRing α] [AddLeftCancelMonoid G] [Finite G] (ψ : AddChar G α) (x : G) : ‖ψ x‖₊ = 1

theorem BohrSet.eq_top_of_two_le_width {G : Type u_1} [AddCommGroup G] {B : BohrSet G} [Finite G] (h : ∀ (ψ : AddChar G ℂ), 2 ≤ B.width ψ) : ↑B = Set.univ

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

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

theorem BohrSet.add_subset_of_ewidth {G : Type u_1} [AddCommGroup G] [Finite G] {B₁ B₂ B₃ : BohrSet G} (h : B₁.ewidth + B₂.ewidth ≤ B₃.ewidth) : ↑B₁ + ↑B₂ ⊆ ↑B₃

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