The universal scale

A measure μ : E → D orders a finite comparison class C by a quasi-order whose classes are the values C.image μ. Bale's universal degree of a member is the position of its class: one plus the number of classes below it, over the number of classes, a rational between zero and one. Universal degrees record positions and nothing else. They are unchanged by any order embedding of the scale, and on a comparison class two measures give the same universal degrees exactly when they induce the same quasi-order. Comparing two measures directly is not invariant under rescaling one of them (Degree.Comparison.forall_preimage_interval_eq_iff), but comparing their universal degrees is, which is what makes a comparison between different adjectives meaningful.

Main definitions

• Degree.relativeRank: the position of a value in a finite scale, as a fraction of the scale.
• Degree.universalDegree: the universal degree of a member of a comparison class under a measure.

Main statements

• Degree.universalDegree_comp: universal degrees are invariant under order embeddings of the scale.
• Degree.ker_universalDegree: on a comparison class, universal degrees are a complete invariant of the quasi-order the measure induces.
• Degree.universalDegree_eq_iff: two members share a universal degree exactly when they are equivalent in Cresswell's sense.

Implementation notes

A comparison class is a Finset, Klein's comparison class made finite so that its classes can be counted. The primary scale, the quotient of the restricted quasi-order, is order-isomorphic to C.image μ, where universal degrees are computed; ker_universalDegree makes the choice of measure immaterial.

References

• [Bal08]
• [Cre76]
• [Kle80]

Positions in a finite scale

def Degree.relativeRank {D : Type u_1} [LinearOrder D] (S : Finset D) (d : D) : ℚ

The relative rank of d in a finite scale S is the share of S at or below it, one plus the number of values below d over the number of values.

Equations

• Degree.relativeRank S d = ↑{x ∈ S | x ≤ d}.card / ↑S.card

theorem Degree.relativeRank_strictMonoOn {D : Type u_1} [LinearOrder D] (S : Finset D) : StrictMonoOn (relativeRank S) ↑S

Relative rank preserves and reflects the order of the scale.

theorem Degree.relativeRank_of_forall_le {D : Type u_1} [LinearOrder D] {S : Finset D} {d : D} (hd : d ∈ S) (h : ∀ x ∈ S, x ≤ d) : relativeRank S d = 1

The top of a scale has relative rank one.

theorem Degree.relativeRank_of_forall_ge {D : Type u_1} [LinearOrder D] {S : Finset D} {d : D} (hd : d ∈ S) (h : ∀ x ∈ S, d ≤ x) : relativeRank S d = 1 / ↑S.card

The bottom of a scale has relative rank one over the size of the scale.

theorem Degree.relativeRank_Icc {N n : ℕ} (hn : n ∈ Finset.Icc 1 N) : relativeRank (Finset.Icc 1 N) n = ↑n / ↑N

On the scale of the numbers from one to N, the relative rank of n is n / N.

Universal degrees

def Degree.universalDegree {D : Type u_1} {E : Type u_3} [LinearOrder D] [DecidableEq D] (μ : E → D) (C : Finset E) (x : E) : ℚ

The universal degree of x under the measure μ on the comparison class C is the relative rank of its class among the classes of C.

Equations

• Degree.universalDegree μ C x = Degree.relativeRank (Finset.image μ C) (μ x)

theorem Degree.universalDegree_lt_iff {D : Type u_1} {E : Type u_3} [LinearOrder D] [DecidableEq D] {μ : E → D} {C : Finset E} {x y : E} (hx : x ∈ C) (hy : y ∈ C) : universalDegree μ C x < universalDegree μ C y ↔ μ x < μ y

Within one comparison class, universal degrees compare as the measures do.

@[simp]

theorem Degree.universalDegree_comp {D : Type u_1} {D' : Type u_2} {E : Type u_3} [LinearOrder D] [DecidableEq D] [LinearOrder D'] [DecidableEq D'] (f : D ↪o D') (μ : E → D) (C : Finset E) : universalDegree (⇑f ∘ μ) C = universalDegree μ C

Universal degrees are invariant under any order embedding of the scale.

theorem Degree.universalDegree_congr {D : Type u_1} {D' : Type u_2} {E : Type u_3} [LinearOrder D] [DecidableEq D] [LinearOrder D'] [DecidableEq D'] {μ : E → D} {C : Finset E} {x : E} {ν : E → D'} (h : ∀ a ∈ C, ∀ b ∈ C, μ a ≤ μ b ↔ ν a ≤ ν b) (hx : x ∈ C) : universalDegree μ C x = universalDegree ν C x

Two measures inducing the same quasi-order on a comparison class give its members the same universal degrees.

theorem Degree.ker_universalDegree {D : Type u_1} {E : Type u_3} [LinearOrder D] [DecidableEq D] (C : Finset E) : (Setoid.ker fun (μ : E → D) (x : ↥C) => universalDegree μ C ↑x) = Setoid.ker fun (μ : E → D) (a b : ↥C) => μ ↑a ≤ μ ↑b

On a comparison class, universal degrees are a complete invariant of the quasi-order a measure induces, so two measures give the same universal degrees exactly when they order the class alike.

theorem Degree.universalDegree_eq_iff {D : Type u_1} {E : Type u_3} [LinearOrder D] [DecidableEq D] {μ : E → D} {C : Finset E} {x y : E} (hx : x ∈ C) (hy : y ∈ C) : universalDegree μ C x = universalDegree μ C y ↔ (cresswellSetoid fun (a b : ↥C) => μ ↑b ≤ μ ↑a) ⟨x, hx⟩ ⟨y, hy⟩

Two members of a comparison class share a universal degree exactly when they are equivalent in [Cre76]'s sense under the restricted quasi-order.

theorem Degree.universalDegree_lt_iff_of_image_eq {D : Type u_1} {E : Type u_3} {F : Type u_4} [LinearOrder D] [DecidableEq D] {μ : E → D} {C : Finset E} {x : E} {ν : F → D} {C' : Finset F} {y : F} (h : Finset.image μ C = Finset.image ν C') (hx : x ∈ C) (hy : y ∈ C') : universalDegree μ C x < universalDegree ν C' y ↔ μ x < ν y

Two primary scales with the same classes compare across as the measures do.

theorem Degree.universalDegree_eq_of_image_eq {D : Type u_1} {E : Type u_3} [LinearOrder D] [DecidableEq D] {μ : E → D} {C C' : Finset E} (h : Finset.image μ C = Finset.image μ C') : universalDegree μ C = universalDegree μ C'

Comparison classes with the same classes give the same universal degrees, so members added to a comparison class, each measuring as one already there, change no universal degree.

theorem Degree.universalDegree_of_forall_le {D : Type u_1} {E : Type u_3} [LinearOrder D] [DecidableEq D] {μ : E → D} {C : Finset E} {x : E} (hx : x ∈ C) (h : ∀ y ∈ C, μ y ≤ μ x) : universalDegree μ C x = 1

A member measuring at least as much as every other has universal degree one.

theorem Degree.universalDegree_of_forall_ge {D : Type u_1} {E : Type u_3} [LinearOrder D] [DecidableEq D] {μ : E → D} {C : Finset E} {x : E} (hx : x ∈ C) (h : ∀ y ∈ C, μ x ≤ μ y) : universalDegree μ C x = 1 / ↑(Finset.image μ C).card

A member measuring at most as much as every other has universal degree one over the number of classes.

theorem Degree.universalDegree_of_image_eq_Icc {E : Type u_3} {C : Finset E} {x : E} {μ : E → ℕ} {N : ℕ} (h : Finset.image μ C = Finset.Icc 1 N) (hx : x ∈ C) : universalDegree μ C x = ↑(μ x) / ↑N

When the classes of a comparison class are the numbers from one to N, a universal degree is the measure over N.