pith. machine review for the scientific record. sign in
def definition def or abbrev

ScaleInvariant

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 116def ScaleInvariant (C : ComparisonOperator) : Prop :=

proof body

Definition body.

 117  ∀ x y lam : ℝ, 0 < x → 0 < y → 0 < lam →
 118    C (lam * x) (lam * y) = C x y
 119
 120/-- **Route-independence (the d'Alembert form)**: the cost of any composite
 121comparison, taken in its symmetric forward-and-backward form on positive
 122ratios, is a polynomial function of the constituent ratio costs.
 123Concretely: assembling a comparison of ratio xy with a comparison of ratio
 124x/y (the symmetric forward+backward decomposition) gives a total cost that
 125is some fixed polynomial in the costs of the individual ratios x and y.
 126The polynomial restriction is the Level-1 regularity assumption; Level 2
 127will replace it with continuity. -/

used by (17)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.