# 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).

## TODO #

• The fact inner_product_geometry.angle (Real.cos θ) (Real.sin θ) = ‖(θ : Real.Angle)‖
@[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 : } (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 : ) {ε : } (hε : |p| / 2 ε) :
= Set.univ
@[simp]
theorem AddCircle.coe_real_preimage_closedBall_period_zero (x : ) (ε : ) :
QuotientAddGroup.mk ⁻¹' 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 : ) (hs : s Metric.closedBall x (|p| / 2)) :
QuotientAddGroup.mk ⁻¹' Metric.closedBall (x) ε s = if ε < |p| / 2 then s else s
theorem AddCircle.norm_div_nat_cast {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 : } (hu : ) :
k, u = p * (k / ↑())
theorem AddCircle.le_add_order_smul_norm_of_isOfFinAddOrder {p : } [hp : Fact (0 < p)] {u : } (hu : ) (hu' : u 0) :
p
theorem UnitAddCircle.norm_eq {x : } :
x = |x - ↑()|