The additive circle as a normed group

We define the normed group structure on AddCircle p, for p : ℝ. For example if p = 1 then: ‖(x : AddCircle 1)‖ = |x - round x| for any x : ℝ (see UnitAddCircle.norm_eq).

Main definitions:

• AddCircle.norm_eq: a characterisation of the norm on AddCircle p

TODO

• The fact InnerProductGeometry.angle (Real.cos θ) (Real.sin θ) = ‖(θ : Real.Angle)‖

@[implicit_reducible]

noncomputable instance AddCircle.instNormedAddCommGroupReal (p : ℝ) : NormedAddCommGroup (AddCircle p)

Equations

• AddCircle.instNormedAddCommGroupReal p = QuotientAddGroup.instNormedAddCommGroup (AddSubgroup.zmultiples p)

@[simp]

theorem AddCircle.norm_coe_mul (p x t : ℝ) : ‖↑(t * x)‖ = |t| * ‖↑x‖

theorem AddCircle.norm_neg_period (p x : ℝ) : ‖↑x‖ = ‖↑x‖

@[simp]

theorem AddCircle.norm_eq_of_zero {x : ℝ} : ‖↑x‖ = |x|

theorem AddCircle.norm_eq (p : ℝ) {x : ℝ} : ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

theorem AddCircle.norm_eq' (p : ℝ) (hp : 0 < p) {x : ℝ} : ‖↑x‖ = p * |p⁻¹ * x - ↑(round (p⁻¹ * x))|

theorem AddCircle.norm_le_half_period (p : ℝ) {x : AddCircle p} (hp : p ≠ 0) : ‖x‖ ≤ |p| / 2

@[simp]

theorem AddCircle.norm_half_period_eq (p : ℝ) : ‖↑(p / 2)‖ = |p| / 2

theorem AddCircle.norm_coe_eq_abs_iff (p : ℝ) {x : ℝ} (hp : p ≠ 0) : ‖↑x‖ = |x| ↔ |x| ≤ |p| / 2

theorem AddCircle.closedBall_eq_univ_of_half_period_le (p : ℝ) (hp : p ≠ 0) (x : AddCircle p) {ε : ℝ} (hε : |p| / 2 ≤ ε) : Metric.closedBall x ε = Set.univ

@[simp]

theorem AddCircle.coe_real_preimage_closedBall_period_zero (x ε : ℝ) : QuotientAddGroup.mk ⁻¹' Metric.closedBall (↑x) ε = Metric.closedBall x ε

theorem AddCircle.coe_real_preimage_closedBall_eq_iUnion (p x ε : ℝ) : QuotientAddGroup.mk ⁻¹' Metric.closedBall (↑x) ε = ⋃ (z : ℤ), Metric.closedBall (x + z • p) ε

theorem AddCircle.coe_real_preimage_closedBall_inter_eq (p : ℝ) {x ε : ℝ} (s : Set ℝ) (hs : s ⊆ Metric.closedBall x (|p| / 2)) : QuotientAddGroup.mk ⁻¹' Metric.closedBall (↑x) ε ∩ s = if ε < |p| / 2 then Metric.closedBall x ε ∩ s else s

theorem AddCircle.norm_div_natCast {p : ℝ} [hp : Fact (0 < p)] {m n : ℕ} : ‖↑(↑m / ↑n * p)‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)

theorem AddCircle.exists_norm_eq_of_isOfFinAddOrder {p : ℝ} [hp : Fact (0 < p)] {u : AddCircle p} (hu : IsOfFinAddOrder u) : ∃ (k : ℕ), ‖u‖ = p * (↑k / ↑(addOrderOf u))

theorem AddCircle.le_add_order_smul_norm_of_isOfFinAddOrder {p : ℝ} [hp : Fact (0 < p)] {u : AddCircle p} (hu : IsOfFinAddOrder u) (hu' : u ≠ 0) : p ≤ addOrderOf u • ‖u‖

theorem UnitAddCircle.norm_eq {x : ℝ} : ‖↑x‖ = |x - ↑(round x)|