def BohrSet.arcSet {G : Type u_1} [AddCommGroup G] {B : BohrSet G} : Set G

Equations

• BohrSet.arcSet = {x : G | ∀ (ψ : AddChar G ℂ), ↑‖InnerProductGeometry.angle (ψ x) 1‖₊ ≤ B.ewidth ψ}

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

theorem BohrSet.mem_arcSet_iff_nnnorm_width {G : Type u_1} [AddCommGroup G] {B : BohrSet G} {x : G} : x ∈ arcSet ↔ ∀ ⦃ψ : AddChar G ℂ⦄, ψ ∈ B.frequencies → ‖InnerProductGeometry.angle (ψ x) 1‖₊ ≤ B.width ψ

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

theorem BohrSet.arcSet_subset_chordSet {G : Type u_1} [AddCommGroup G] {B : BohrSet G} [Finite G] : arcSet ⊆ ↑B

theorem BohrSet.chordSet_subset_smul_arcSet {G : Type u_1} [AddCommGroup G] {B : BohrSet G} [Finite G] : ↑B ⊆ arcSet