English
For l, r in natural numbers, BalancedSz(l, r) holds exactly when either l + r ≤ 1, or l ≤ δ r and r ≤ δ l, where δ is a fixed balance constant.
Русский
Для целых чисел l и r балансирование размеров выполняется либо при l + r ≤ 1, либо при l ≤ δ r и r ≤ δ l, где δ — константа балансировки.
LaTeX
$$$$\operatorname{BalancedSz}(l,r) \iff l + r \le 1 \; \lor\; (l \le \delta r) \land (r \le \delta l).$$$$
Lean4
/-- The `BalancedSz l r` asserts that a hypothetical tree with children of sizes `l` and `r` is
balanced: either `l ≤ δ * r` and `r ≤ δ * r`, or the tree is trivial with a singleton on one side
and nothing on the other. -/
def BalancedSz (l r : ℕ) : Prop :=
l + r ≤ 1 ∨ l ≤ delta * r ∧ r ≤ delta * l
