Scale granularity

A granularity function of width w maps each degree to an interval of width w that contains it. The grain of width ε is the granularity function that reports each degree by the nearest multiple of ε: degrees with the same nearest multiple are indistinguishable, and the cell of a degree is the half-open interval of width ε centred on that multiple. Krifka builds levels of precision this way, Sauerland and Stateva define granularity functions by the properties collected in IsGranularity, and Deo and Thomas take the cells of a grain as the answers to a degree question.

A finer grain is a narrower one, not a refinement. No cell of a wider granularity function fits inside a cell of a narrower one, and a grain refines the grain k times as wide exactly when k is odd, so halving the width never refines. Around a common multiple of two widths the cells are nested.

Main definitions

• Degree.IsGranularity: a granularity function of a given width.
• Degree.grain: the partition of the scale by nearest multiple of ε.
• Degree.representative: the nearest multiple of ε.

Main results

• Degree.cell_grain: a cell is the half-open interval of width ε centred on its representative.
• Degree.IsGranularity.not_subset: a cell of a wider granularity function never fits inside a cell of a narrower one.
• Degree.isGranularity_zero_iff: the granularity function of width zero is the exact reading, every cell a single degree.
• Degree.cell_grain_subset_cell_grain: around a common multiple, a finer cell lies inside a coarser one.
• Degree.grain_le_grain_iff_odd: the grain of width ε refines the grain of width k * ε exactly when k is odd.

Implementation notes

Cells are half-open, the only choice of endpoints that partitions the scale; Sauerland and Stateva write closed intervals and Thomas and Deo open ones. IsGranularity states the width by placing each cell between the open and the closed interval of that width, which leaves the endpoints open, as Thomas and Deo recommend, and needs no sSup, which ℚ lacks.

References

• [Kri07a]
• [SS11]
• [TD20]
• [DT25]

structure Degree.IsGranularity {D : Type u_1} [AddCommGroup D] [LinearOrder D] (γ : D → Set D) (w : D) : Prop

A granularity function of width w maps each degree to a set that contains it and lies between the open and the closed interval of width w with a common left end.

• mem_self (s : D) : s ∈ γ s

  Every degree lies in its own cell.

• exists_Ioo_subset_subset_Icc (s : D) : ∃ (a : D), Set.Ioo a (a + w) ⊆ γ s ∧ γ s ⊆ Set.Icc a (a + w)

  Every cell is an interval of width w, whichever of its endpoints it contains.

theorem Degree.IsGranularity.ordConnected {D : Type u_1} [AddCommGroup D] [LinearOrder D] {γ : D → Set D} {w : D} (h : IsGranularity γ w) (s : D) : (γ s).OrdConnected

The cells of a granularity function are convex.

theorem Degree.isGranularity_zero_iff {D : Type u_1} [AddCommGroup D] [LinearOrder D] {γ : D → Set D} : IsGranularity γ 0 ↔ γ = fun (s : D) => {s}

The granularity function of width zero is the exact reading, every cell a single degree.

theorem Degree.IsGranularity.nonneg {D : Type u_1} [AddCommGroup D] [LinearOrder D] {γ : D → Set D} {w : D} [IsOrderedAddMonoid D] (h : IsGranularity γ w) : 0 ≤ w

theorem Degree.IsGranularity.not_subset {D : Type u_1} [AddCommGroup D] [LinearOrder D] {γ₁ γ₂ : D → Set D} {w₁ w₂ : D} [IsOrderedAddMonoid D] [DenselyOrdered D] (h₁ : IsGranularity γ₁ w₁) (h₂ : IsGranularity γ₂ w₂) (hlt : w₁ < w₂) (s t : D) : ¬γ₂ t ⊆ γ₁ s

A cell of a wider granularity function never lies inside a cell of a narrower one.

def Degree.grain {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] (ε : α) : Setoid α

The grain of width ε identifies two degrees when they have the same nearest multiple of ε.

Equations

• Degree.grain ε = Setoid.ker fun (d : α) => round (d / ε)

def Degree.representative {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] (ε d : α) : α

The representative of d at width ε is the nearest multiple of ε.

Equations

• Degree.representative ε d = round (d / ε) • ε

theorem Degree.grain_iff {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε d d' : α} : (grain ε) d d' ↔ round (d / ε) = round (d' / ε)

theorem Degree.representative_mem_zmultiples {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] (ε d : α) : representative ε d ∈ AddSubgroup.zmultiples ε

theorem Degree.preimage_representative_of_notMem {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε d : α} (hd : d ∉ AddSubgroup.zmultiples ε) : representative ε ⁻¹' {d} = ∅

Only scale points are reported.

theorem Degree.representative_eq_self_of_mem_zmultiples {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε d : α} (hε : ε ≠ 0) (hd : d ∈ AddSubgroup.zmultiples ε) : representative ε d = d

theorem Degree.grain_iff_representative {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε d d' : α} [IsStrictOrderedRing α] (hε : ε ≠ 0) : (grain ε) d d' ↔ representative ε d = representative ε d'

theorem Degree.abs_sub_representative_le {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε : α} [IsStrictOrderedRing α] (hε : 0 < ε) (d : α) : |d - representative ε d| ≤ ε / 2

theorem Degree.abs_sub_representative_le_abs_sub {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε : α} [IsStrictOrderedRing α] (hε : ε ≠ 0) (d : α) (n : ℤ) : |d - representative ε d| ≤ |d - n • ε|

The representative of d is the multiple of ε nearest to d.

theorem Degree.cell_grain {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε : α} [IsStrictOrderedRing α] (hε : 0 < ε) (d : α) : (grain ε).cell d = Set.Ico (representative ε d - ε / 2) (representative ε d + ε / 2)

The cell of d is the half-open interval of width ε centred on its representative.

theorem Degree.abs_sub_representative_eq_half_iff {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε : α} [IsStrictOrderedRing α] (hε : 0 < ε) {d : α} : |d - representative ε d| = ε / 2 ↔ d ∈ AddSubgroup.zmultiples (ε / 2) ∧ d ∉ AddSubgroup.zmultiples ε

The grain moves a degree by exactly half its width at the points that halving the width adds to the scale.

theorem Degree.preimage_representative {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε : α} [IsStrictOrderedRing α] (hε : 0 < ε) {d : α} (hd : d ∈ AddSubgroup.zmultiples ε) : representative ε ⁻¹' {d} = Set.Ico (d - ε / 2) (d + ε / 2)

The degrees reported as a scale point are its cell, the half-open interval of the grain's width centred on it.

theorem Degree.abs_sub_lt_of_grain {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε d d' : α} [IsStrictOrderedRing α] (hε : 0 < ε) (h : (grain ε) d d') : |d - d'| < ε

Two degrees the grain of width ε identifies are less than ε apart.

theorem Degree.isGranularity_cell {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε : α} [IsStrictOrderedRing α] (hε : 0 < ε) : IsGranularity (grain ε).cell ε

theorem Degree.cell_grain_subset_cell_grain {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε₁ ε₂ d : α} [IsStrictOrderedRing α] (hε₁ : 0 < ε₁) (h : ε₁ ≤ ε₂) (h₁ : d ∈ AddSubgroup.zmultiples ε₁) (h₂ : d ∈ AddSubgroup.zmultiples ε₂) : (grain ε₁).cell d ⊆ (grain ε₂).cell d

Around a common multiple of two widths, the cell of the finer grain lies inside the cell of the coarser one.

theorem Degree.grain_le_grain_of_odd {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε : α} [IsStrictOrderedRing α] (j : ℕ) : grain ε ≤ grain (↑(2 * j + 1) * ε)

The grain of width ε refines the grain of any odd multiple of its width.

theorem Degree.not_grain_le_grain_of_even {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε : α} [IsStrictOrderedRing α] (hε : 0 < ε) {j : ℕ} (hj : 0 < j) : ¬grain ε ≤ grain (↑(2 * j) * ε)

The grain of width ε refines no grain of an even multiple of its width, since the boundary j * ε of the coarser grain is the centre of a cell of the finer one.

theorem Degree.grain_le_grain_iff_odd {α : Type u_1} [Field α] [LinearOrder α] [FloorRing α] {ε : α} [IsStrictOrderedRing α] (hε : 0 < ε) {k : ℕ} (hk : 0 < k) : grain ε ≤ grain (↑k * ε) ↔ Odd k

The grain of width ε refines the grain of width k * ε exactly when k is odd.