Documentation

Mathlib.Analysis.Normed.Group.AddCircle

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: #

TODO #

@[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_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_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 : AddCircle p} (hu : IsOfFinAddOrder u) :
k, u = p * (k / ↑(addOrderOf u))
theorem UnitAddCircle.norm_eq {x : } :
x = |x - ↑(round x)|