mathlib3 documentation

analysis.normed.group.add_circle

The additive circle as a normed group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions: #

TODO #

@[simp]
theorem add_circle.norm_coe_mul (p x t : ) :
@[simp]
theorem add_circle.norm_eq (p : ) {x : } :
theorem add_circle.norm_eq' (p : ) (hp : 0 < p) {x : } :
theorem add_circle.norm_le_half_period (p : ) {x : add_circle p} (hp : p 0) :
@[simp]
theorem add_circle.norm_half_period_eq (p : ) :
(p / 2) = |p| / 2
theorem add_circle.norm_coe_eq_abs_iff (p : ) {x : } (hp : p 0) :
theorem add_circle.closed_ball_eq_univ_of_half_period_le (p : ) (hp : p 0) (x : add_circle p) {ε : } (hε : |p| / 2 ε) :
theorem add_circle.norm_div_nat_cast {p : } [hp : fact (0 < p)] {m n : } :
(m / n * p) = p * ((linear_order.min (m % n) (n - m % n)) / n)