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

add_circle.norm_eq: a characterisation of the norm on add_circle p

TODO #

The fact inner_product_geometry.angle (real.cos θ) (real.sin θ) = ‖(θ : real.angle)‖

source

@[protected, instance]

noncomputable def add_circle.normed_add_comm_group (p : ℝ) :

normed_add_comm_group (add_circle p)

Equations

add_circle.normed_add_comm_group p = (add_subgroup.zmultiples p).normed_add_comm_group_quotient

source

@[simp]

theorem add_circle.norm_coe_mul (p x t : ℝ) :

‖↑(t * x)‖ = |t| * ‖↑x‖

source

theorem add_circle.norm_neg_period (p x : ℝ) :

‖↑x‖ = ‖↑x‖

source

@[simp]

theorem add_circle.norm_eq_of_zero {x : ℝ} :

‖↑x‖ = |x|

source

theorem add_circle.norm_eq (p : ℝ) {x : ℝ} :

‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

source

theorem add_circle.norm_eq' (p : ℝ) (hp : 0 < p) {x : ℝ} :

‖↑x‖ = p * |p⁻¹ * x - ↑(round (p⁻¹ * x))|

source

theorem add_circle.norm_le_half_period (p : ℝ) {x : add_circle p} (hp : p ≠ 0) :

‖x‖ ≤ |p| / 2

source

@[simp]

theorem add_circle.norm_half_period_eq (p : ℝ) :

‖↑(p / 2)‖ = |p| / 2

source

theorem add_circle.norm_coe_eq_abs_iff (p : ℝ) {x : ℝ} (hp : p ≠ 0) :

‖↑x‖ = |x| ↔ |x| ≤ |p| / 2

source

theorem add_circle.closed_ball_eq_univ_of_half_period_le (p : ℝ) (hp : p ≠ 0) (x : add_circle p) {ε : ℝ} (hε : |p| / 2 ≤ ε) :

metric.closed_ball x ε = set.univ

source

@[simp]

theorem add_circle.coe_real_preimage_closed_ball_period_zero (x ε : ℝ) :

coe ⁻¹' metric.closed_ball ↑x ε = metric.closed_ball x ε

source

theorem add_circle.coe_real_preimage_closed_ball_eq_Union (p x ε : ℝ) :

coe ⁻¹' metric.closed_ball ↑x ε = ⋃ (z : ℤ), metric.closed_ball (x + z • p) ε

source

theorem add_circle.coe_real_preimage_closed_ball_inter_eq (p : ℝ) {x ε : ℝ} (s : set ℝ) (hs : s ⊆ metric.closed_ball x (|p| / 2)) :

coe ⁻¹' metric.closed_ball ↑x ε ∩ s = ite (ε < |p| / 2) (metric.closed_ball x ε ∩ s) s

source

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)

source

theorem add_circle.exists_norm_eq_of_fin_add_order {p : ℝ} [hp : fact (0 < p)] {u : add_circle p} (hu : is_of_fin_add_order u) :

∃ (k : ℕ), ‖u‖ = p * (↑k / ↑(add_order_of u))

source

theorem add_circle.le_add_order_smul_norm_of_is_of_fin_add_order {p : ℝ} [hp : fact (0 < p)] {u : add_circle p} (hu : is_of_fin_add_order u) (hu' : u ≠ 0) :

p ≤ add_order_of u • ‖u‖

source

theorem unit_add_circle.norm_eq {x : ℝ} :

‖↑x‖ = |x - ↑(round x)|