Common.Real.Floor

A collection of useful definitions and theorems around the floor function.

theorem Real.Floor.fract_mem_Ico_zero_one (x : ℝ) : Int.fract x ∈ Set.Ico 0 1

The fractional portion of any real number is always in [0, 1).

Hermite's Identity

Definitions and theorems in support of proving Hermite's identity.

def Real.Floor.Hermite.partition (n : ℕ) (i : ℕ) : Set ℝ

A partition of [0, 1) that looks as follows:

[0, 1/n), [1/n, 2/n), ..., [(n-1)/n, 1)

This is expected to be used as an indexing function of a union of sets, e.g. ⋃ i ∈ Finset.range n, partition n i.

Equations

• Real.Floor.Hermite.partition n i = Set.Ico (↑i / ↑n) ((↑i + 1) / ↑n)

theorem Real.Floor.Hermite.fract_mem_partition (r : ℝ) (hr : r ∈ Set.Ico 0 1) (n : ℕ) : ∃ j < n, r ∈ Set.Ico (↑j / ↑n) ((↑j + 1) / ↑n)

The fractional portion of any real number always exists in some member of the indexed family of sets formed by any partition.

theorem Real.Floor.Hermite.partition_subset_Ico_zero_one {n : ℕ} : ⋃ i ∈ Finset.range n, Real.Floor.Hermite.partition n i ⊆ Set.Ico 0 1

The indexed union of the family of sets of a partition is a subset of [0, 1).

theorem Real.Floor.Hermite.Ico_zero_one_subset_partition {n : ℕ} : Set.Ico 0 1 ⊆ ⋃ i ∈ Finset.range n, Real.Floor.Hermite.partition n i

[0, 1) is a subset of the indexed union of the family of sets of a partition.

theorem Real.Floor.Hermite.partition_eq_Ico_zero_one {n : ℕ} : ⋃ i ∈ Finset.range n, Real.Floor.Hermite.partition n i = Set.Ico 0 1

The indexed union of the family of sets of a partition is equal to [0, 1).

theorem Real.Floor.floor_mul_eq_sum_range_floor_add_index_div (n : ℕ) (x : ℝ) : ⌊↑n * x⌋ = Finset.sum (Finset.range n) fun (i : ℕ) => ⌊x + ↑i / ↑n⌋

Hermite's Identity

The following decomposes the floor of a multiplication into a sum of floors.