Floors and decompositions into intervals

A point of [0, n) in an ordered ring with a floor operation is the sum of an index in Fin n and a remainder in [0, 1). This describes, for example, time along one of the finitely many edges in a polygonal boundary parametrization. In the same way, a 1-periodic function is determined by its values on [0, 1): it takes the same value at t and at the fractional part of t.

For a step δ > 0 in a linearly ordered field with an integer floor, the multiples of δ cut the line into the closed intervals [δ m, δ (m + 1)] with m ∈ ℤ. Every point x lies in the interval indexed by ⌊x / δ⌋, and an interval meeting [-R, R] has its index between ⌈-R / δ⌉ - 1 and ⌊R / δ⌋.

Main results

• TauCeti.exists_eq_natCast_add_of_mem_Ico: a point of [0, n) is an index in Fin n plus a remainder in [0, 1).
• Function.Periodic.apply_fract: a 1-periodic function takes the same value at t and at its fractional part Int.fract t.
• TauCeti.mem_Icc_mul_floor_div: x ∈ [δ ⌊x / δ⌋, δ (⌊x / δ⌋ + 1)].
• TauCeti.mem_Icc_ceil_floor_of_mem_Icc: if x ∈ [δ m, δ (m + 1)] and |x| ≤ R, then m ∈ [⌈-R / δ⌉ - 1, ⌊R / δ⌋].
• TauCeti.abs_sub_lt_one_div_of_natFloor_mul_eq: for t > 0, nonnegative elements a, b with ⌊a * t⌋₊ = ⌊b * t⌋₊ differ by less than 1 / t.

theorem TauCeti.exists_eq_natCast_add_of_mem_Ico {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {n : ℕ} {t : R} (ht : t ∈ Set.Ico 0 ↑n) : ∃ (j : Fin n), ∃ u ∈ Set.Ico 0 1, t = ↑↑j + u

A point of [0, n) is an index in Fin n plus a remainder in [0, 1).

theorem Function.Periodic.apply_fract {R : Type u_1} {β : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {f : R → β} (hf : Periodic f 1) (t : R) : f (Int.fract t) = f t

A 1-periodic function takes the same value at t and at its fractional part.

theorem TauCeti.mem_Icc_mul_floor_div {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] {δ : K} (hδ : 0 < δ) (x : K) : x ∈ Set.Icc (δ * ↑⌊x / δ⌋) (δ * (↑⌊x / δ⌋ + 1))

For a step δ > 0, the point x lies in the interval [δ m, δ (m + 1)] with m = ⌊x / δ⌋.

theorem TauCeti.mem_Icc_ceil_floor_of_mem_Icc {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] {δ : K} (hδ : 0 < δ) {R x : K} {m : ℤ} (hx : x ∈ Set.Icc (δ * ↑m) (δ * (↑m + 1))) (hxR : |x| ≤ R) : m ∈ Set.Icc (⌈-R / δ⌉ - 1) ⌊R / δ⌋

For a step δ > 0, an interval [δ m, δ (m + 1)] that meets [-R, R] has its index m in the finite range [⌈-R / δ⌉ - 1, ⌊R / δ⌋].

theorem TauCeti.abs_sub_lt_one_div_of_natFloor_mul_eq {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] {a b t : K} (ht : 0 < t) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : ⌊a * t⌋₊ = ⌊b * t⌋₊) : |a - b| < 1 / t

For t > 0, two nonnegative elements a, b of an ordered field with the same natural floor of x * t differ by less than 1 / t: on the nonnegative half-line the cells of the grid of scale t have side 1 / t.