Ceilings and floors of quotients by a step

For a step τ > 0 in a linearly ordered division semiring, the multiples n τ of the step lying in a half-open interval [s, t) are those with n ∈ [⌈s / τ⌉₊, ⌈t / τ⌉₊). With ordered subtraction and s ≤ t, there are strictly fewer than (t - s) / τ + 1 of them. These are the index counts of time discretizations with step τ. The counting bound also holds for τ = 0.

Dually, for B > 0 and any natural degree bound n, multiplying B < ⌊B⌋₊ + 1 by n / B < ⌊n / B⌋₊ + 1 gives n < (⌊B⌋₊ + 1) * (⌊n / B⌋₊ + 1), and in particular n < (2 * ⌊B⌋₊ + 1) * (⌊n / B⌋₊ + 1). This includes n = 0 and B < 1, and counts the available jet conditions on an integer interval of radius B.

Main results

• TauCeti.natCast_ceil_div_sub_ceil_div_lt: ⌈t / τ⌉₊ - ⌈s / τ⌉₊ < (t - s) / τ + 1.
• TauCeti.mem_Ico_ceil_div_iff: n ∈ [⌈s / τ⌉₊, ⌈t / τ⌉₊) if and only if n τ ∈ [s, t).
• TauCeti.exists_pos_nat_mul_bounds: a positive multiple N a lies in (t, t + a].
• TauCeti.pairwiseDisjoint_Ico_ceil_div: the index sets [⌈sᵢ / τ⌉₊, ⌈tᵢ / τ⌉₊) are pairwise disjoint whenever the intervals (sᵢ, tᵢ] are.
• TauCeti.card_biUnion_Ico_ceil_div_le: the union of these index sets over k intervals has at most (∑ᵢ (tᵢ - sᵢ)) / τ + k elements.
• TauCeti.lt_floor_add_one_mul_floor_div_add_one: n < (⌊B⌋₊ + 1) * (⌊n / B⌋₊ + 1) for B > 0.
• TauCeti.lt_two_mul_floor_add_one_mul_floor_div_add_one: n < (2 * ⌊B⌋₊ + 1) * (⌊n / B⌋₊ + 1) for B > 0.

theorem TauCeti.natCast_ceil_div_sub_ceil_div_lt {K : Type u_1} [DivisionSemiring K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {τ s t : K} [Sub K] [OrderedSub K] (hτ : 0 ≤ τ) (hst : s ≤ t) : ↑(⌈t / τ⌉₊ - ⌈s / τ⌉₊) < (t - s) / τ + 1

For a nonnegative step τ and s ≤ t, the indices in [⌈s / τ⌉₊, ⌈t / τ⌉₊) number strictly less than (t - s) / τ + 1. This holds for both ordinary and truncated subtraction.

theorem TauCeti.mem_Ico_ceil_div_iff {K : Type u_1} [DivisionSemiring K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {τ s t : K} (hτ : 0 < τ) {n : ℕ} : n ∈ Finset.Ico ⌈s / τ⌉₊ ⌈t / τ⌉₊ ↔ ↑n * τ ∈ Set.Ico s t

For a step τ > 0, an index n lies in [⌈s / τ⌉₊, ⌈t / τ⌉₊) exactly when the multiple n τ lies in [s, t).

theorem TauCeti.pairwiseDisjoint_Ico_ceil_div {K : Type u_1} [DivisionSemiring K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {τ : K} (hτ : 0 < τ) {ι : Type u_2} {s t : ι → K} {S : Set ι} (h : S.PairwiseDisjoint fun (i : ι) => Set.Ioc (s i) (t i)) : S.PairwiseDisjoint fun (i : ι) => Finset.Ico ⌈s i / τ⌉₊ ⌈t i / τ⌉₊

For a step τ > 0, the index sets [⌈sᵢ / τ⌉₊, ⌈tᵢ / τ⌉₊) of the multiples of τ in [sᵢ, tᵢ) are pairwise disjoint whenever the intervals (sᵢ, tᵢ] are.

theorem TauCeti.card_biUnion_Ico_ceil_div_le {K : Type u_1} [DivisionSemiring K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {τ : K} [Sub K] [OrderedSub K] (hτ : 0 ≤ τ) {ι : Type u_2} (I : Finset ι) {s t : ι → K} (hst : ∀ i ∈ I, s i ≤ t i) : ↑(I.biUnion fun (i : ι) => Finset.Ico ⌈s i / τ⌉₊ ⌈t i / τ⌉₊).card ≤ (∑ i ∈ I, (t i - s i)) / τ + ↑I.card

For 0 ≤ τ and sᵢ ≤ tᵢ for k indices i, the union ⋃ᵢ [⌈sᵢ / τ⌉₊, ⌈tᵢ / τ⌉₊) has at most (∑ᵢ (tᵢ - sᵢ)) / τ + k elements. The intervals need not be disjoint.

theorem TauCeti.lt_floor_add_one_mul_floor_div_add_one {K : Type u_1} [DivisionSemiring K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {B : K} (hB : 0 < B) (n : ℕ) : n < (⌊B⌋₊ + 1) * (⌊↑n / B⌋₊ + 1)

For B > 0 and any n : ℕ, (⌊B⌋₊ + 1) * (⌊n / B⌋₊ + 1) strictly exceeds n, including when n = 0 or B < 1.

theorem TauCeti.lt_two_mul_floor_add_one_mul_floor_div_add_one {K : Type u_1} [DivisionSemiring K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {B : K} (hB : 0 < B) (n : ℕ) : n < (2 * ⌊B⌋₊ + 1) * (⌊↑n / B⌋₊ + 1)

For B > 0 and any n : ℕ, (2 * ⌊B⌋₊ + 1) * (⌊n / B⌋₊ + 1) strictly exceeds n: an integer interval [-⌊B⌋₊, ⌊B⌋₊] with derivative orders up to ⌊n / B⌋₊ has more than n point-order pairs, also when n = 0 or B < 1.

theorem TauCeti.exists_pos_nat_mul_bounds {K : Type u_1} [DivisionSemiring K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {t a : K} (ht : 0 ≤ t) (ha : 0 < a) : ∃ (N : ℕ), 1 ≤ N ∧ t < ↑N * a ∧ ↑N * a ≤ t + a

For a nonnegative t and positive a, some positive multiple N a lies in (t, t + a].