Apostol.Chapter_1_11

theorem Apostol.Chapter_1_11.exercise_4a (x : ℝ) (n : ℤ) : ⌊x + ↑n⌋ = ⌊x⌋ + n

Exercise 4a

⌊x + n⌋ = ⌊x⌋ + n for every integer n.

theorem Apostol.Chapter_1_11.exercise_4b_1 (x : ℤ) : ⌊-x⌋ = -⌊x⌋

Exercise 4b.1

⌊-x⌋ = -⌊x⌋ if x is an integer.

theorem Apostol.Chapter_1_11.exercise_4b_2 (x : ℝ) (h : ∃ (n : ℤ), x ∈ Set.Ioo (↑n) (↑n + 1)) : ⌊-x⌋ = -⌊x⌋ - 1

Exercise 4b.2

⌊-x⌋ = -⌊x⌋ - 1 otherwise.

theorem Apostol.Chapter_1_11.exercise_4c (x : ℝ) (y : ℝ) : ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ ∨ ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ + 1

Exercise 4c

⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ or ⌊x⌋ + ⌊y⌋ + 1.

theorem Apostol.Chapter_1_11.exercise_5 (n : ℕ) (x : ℝ) : ⌊↑n * x⌋ = Finset.sum (Finset.range n) fun (i : ℕ) => ⌊x + ↑i / ↑n⌋

Exercise 5

The formulas in Exercises 4(d) and 4(e) suggest a generalization for ⌊nx⌋. State and prove such a generalization.

theorem Apostol.Chapter_1_11.exercise_4d (x : ℝ) : ⌊2 * x⌋ = ⌊x⌋ + ⌊x + 1 / 2⌋

Exercise 4d

⌊2x⌋ = ⌊x⌋ + ⌊x + 1/2⌋

theorem Apostol.Chapter_1_11.exercise_4e (x : ℝ) : ⌊3 * x⌋ = ⌊x⌋ + ⌊x + 1 / 3⌋ + ⌊x + 2 / 3⌋

Exercise 4e

⌊3x⌋ = ⌊x⌋ + ⌊x + 1/3⌋ + ⌊x + 2/3⌋

theorem Apostol.Chapter_1_11.exercise_7b {a : ℕ} {b : ℕ} (ha : a > 0) (hb : b > 0) (hp : Nat.Coprime a b) : (Finset.sum (Finset.filter (fun (x : ℕ) => x > 0) (Finset.range b)) fun (n : ℕ) => ⌊↑n * ↑a / ↑b⌋) = (↑a - 1) * (↑b - 1) / 2

Exercise 7b

If a and b are positive integers with no common factor, we have the formula ∑_{n=1}^{b-1} ⌊na / b⌋ = ((a - 1)(b - 1)) / 2. When b = 1, the sum on the left is understood to be 0.

Derive the result analytically as follows: By changing the index of summation, note that Σ_{n=1}^{b-1} ⌊na / b⌋ = Σ_{n=1}^{b-1} ⌊a(b - n) / b⌋. Now apply Exercises 4(a) and (b) to the bracket on the right.

theorem Apostol.Chapter_1_11.exercise_8 : True

Exercise 8

Let S be a set of points on the real line. The characteristic function of S is, by definition, the function Χ such that Χₛ(x) = 1 for every x in S, and Χₛ(x) = 0 for those x not in S. Let f be a step function which takes the constant value cₖ on the kth open subinterval Iₖ of some partition of an interval [a, b]. Prove that for each x in the union I₁ ∪ I₂ ∪ ⋯ ∪ Iₙ we have

f(x) = ∑_{k=1}^n cₖΧ_{Iₖ}(x).

This property is described by saying that every step function is a linear combination of characteristic functions of intervals.