English
From a valid balance structure, one obtains a bound 2·size r ≤ 9·size l + 5 or size r ≤ 3.
Русский
Из корректной структуры баланса следует неравенство 2·размер правого поддерева ≤ 9·размер левого поддерева + 5 или размер правого поддерева ≤ 3.
LaTeX
$$$ \forall l,r.\ BalancedSz(l,r) \Rightarrow 2 \cdot |r| \le 9 \cdot |l| + 5 \;
\lor\; |r| \le 3 $$$
Lean4
theorem balance'_lemma {α l l' r r'} (H1 : BalancedSz l' r')
(H2 : Nat.dist (@size α l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l') :
2 * @size α r ≤ 9 * size l + 5 ∨ size r ≤ 3 :=
by
suffices @size α r ≤ 3 * (size l + 1) by cutsat
rcases H2 with (⟨hl, rfl⟩ | ⟨hr, rfl⟩) <;> rcases H1 with (h | ⟨_, h₂⟩)
· exact le_trans (Nat.le_add_left _ _) (le_trans h (Nat.le_add_left _ _))
· exact le_trans h₂ (Nat.mul_le_mul_left _ <| le_trans (Nat.dist_tri_right _ _) (Nat.add_le_add_left hl _))
· exact le_trans (Nat.dist_tri_left' _ _) (le_trans (add_le_add hr (le_trans (Nat.le_add_left _ _) h)) (by cutsat))
· rw [Nat.mul_succ]
exact le_trans (Nat.dist_tri_right' _ _) (add_le_add h₂ (le_trans hr (by decide)))
