English
If the edge lengths of boxes I and J are proportionally related by a common factor r (i.e., I.upper i − I.lower i = (J.upper i − J.lower i)/r for all i), then the distortions of I and J are equal.
Русский
Если длины рёбер коробок I и J пропорциональны общему множителю r (для каждой координаты i выполняется I.upper i − I.lower i = (J.upper i − J.lower i)/r), то и искажения I и J совпадают.
LaTeX
$$$$\forall I,J:\; (\forall i, \ I.upper(i)-I.lower(i) = (J.upper(i)-J.lower(i))/r) \Rightarrow \operatorname{distortion}(I) = \operatorname{distortion}(J).$$$$
Lean4
theorem distortion_eq_of_sub_eq_div {I J : Box ι} {r : ℝ}
(h : ∀ i, I.upper i - I.lower i = (J.upper i - J.lower i) / r) : distortion I = distortion J :=
by
simp only [distortion, nndist_pi_def, Real.nndist_eq', h, map_div₀]
congr 1 with i
have : 0 < r := by
by_contra hr
have := div_nonpos_of_nonneg_of_nonpos (sub_nonneg.2 <| J.lower_le_upper i) (not_lt.1 hr)
rw [← h] at this
exact this.not_gt (sub_pos.2 <| I.lower_lt_upper i)
have hn0 := (map_ne_zero Real.nnabs).2 this.ne'
simp_rw [NNReal.finset_sup_div, div_div_div_cancel_right₀ hn0]
