English
The distortion of a box I is defined as the maximum over all coordinates i of the ratio of the total box length (distance between I.lower and I.upper) to the length of the i-th edge (distance between I.lower i and I.upper i).
Русский
Искажение коробки I есть максимум по всем координатам i от отношения расстояния между концами коробки к длине ребра по координате i.
LaTeX
$$$$\operatorname{distortion}(I) = \ Finset.univ \!\!\.\!\!\sup i : ι \; \frac{\operatorname{nndist}(I.lower,I.upper)}{\operatorname{nndist}(I.lower(i),I.upper(i))}.$$$$
Lean4
/-- The distortion of a box `I` is the maximum of the ratios of the lengths of its edges.
It is defined as the maximum of the ratios
`nndist I.lower I.upper / nndist (I.lower i) (I.upper i)`. -/
def distortion (I : Box ι) : ℝ≥0 :=
Finset.univ.sup fun i : ι ↦ nndist I.lower I.upper / nndist (I.lower i) (I.upper i)
