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

source
@[protected, instance]
noncomputable def add_circle.normed_add_comm_group (p : ℝ) :
normed_add_comm_group (add_circle p)
Equations
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)|