Large rectangles in separable and bi-monotone comparison trees

A separable comparison tests whether the sum of one score from each side meets a threshold. More generally, a bi-monotone comparison combines one real score from each side using a Boolean kernel that is monotone in each score separately. The scores may be arbitrary real-valued functions; neither distinct scores nor linearity is required. Every nonempty finite product domain contains a rectangle routed to one leaf whose sides lose at most the structural leaf count of the tree.

Main definitions

• Cslib.BiMonotoneComparison: a comparison whose Boolean kernel is monotone in each real score separately.
• Cslib.BiMonotoneComparison.ofMax, Cslib.BiMonotoneComparison.ofMin: threshold comparisons of the maximum and minimum of two scores.
• Cslib.SeparableComparison: a threshold comparison of the sum of two separate scores.

Main results

• Cslib.BiMonotoneComparison.exists_rectangle, Cslib.SeparableComparison.exists_rectangle: the finite quantile alternative.
• Cslib.DecisionTree.exists_leaf_rectangle_biMonotone, Cslib.DecisionTree.exists_leaf_rectangle: a rectangle reaches one leaf, with side losses bounded by the number of leaves.
• Cslib.DecisionTree.card_mul_le_mul_leafCount_sq_biMonotone, Cslib.DecisionTree.card_mul_le_mul_leafCount_sq: a monochromatic-area bound forces many leaves.

References

• Threshold Circuits as Decision Trees and Finite-State Programs, Lemma 2.1, Theorem 2.2, and Theorem 2.6

structure Cslib.BiMonotoneComparison (X : Type u_1) (Y : Type u_2) : Type (max u_1 u_2)

A bi-monotone comparison applies a Boolean combiner that is monotone in each real score separately. Queries with a nonincreasing score direction are represented by negating that score.

• left : X → ℝ

  The left score.

• right : Y → ℝ

  The right score.

• kernel : ℝ → ℝ → Bool

  The Boolean combiner of the two scores.

• monotone_left (b : ℝ) : Monotone fun (a : ℝ) => self.kernel a b

  The combiner is monotone in the left score for each fixed right score.

• monotone_right (a : ℝ) : Monotone fun (b : ℝ) => self.kernel a b

  The combiner is monotone in the right score for each fixed left score.

def Cslib.BiMonotoneComparison.eval {X : Type u_1} {Y : Type u_2} (q : BiMonotoneComparison X Y) (x : X) (y : Y) : Bool

The answer to a bi-monotone comparison.

noncomputable def Cslib.BiMonotoneComparison.ofMax {X : Type u_1} {Y : Type u_2} (left : X → ℝ) (right : Y → ℝ) (threshold : ℝ) : BiMonotoneComparison X Y

Compare the maximum of two scores against a threshold: the disjunction of one left-only and one right-only threshold.

@[simp]

theorem Cslib.BiMonotoneComparison.eval_ofMax {X : Type u_1} {Y : Type u_2} (left : X → ℝ) (right : Y → ℝ) (threshold : ℝ) (x : X) (y : Y) : (ofMax left right threshold).eval x y = decide (threshold ≤ max (left x) (right y))

noncomputable def Cslib.BiMonotoneComparison.ofMin {X : Type u_1} {Y : Type u_2} (left : X → ℝ) (right : Y → ℝ) (threshold : ℝ) : BiMonotoneComparison X Y

Compare the minimum of two scores against a threshold: the conjunction of one left-only and one right-only threshold.

@[simp]

theorem Cslib.BiMonotoneComparison.eval_ofMin {X : Type u_1} {Y : Type u_2} (left : X → ℝ) (right : Y → ℝ) (threshold : ℝ) (x : X) (y : Y) : (ofMin left right threshold).eval x y = decide (threshold ≤ min (left x) (right y))

theorem Cslib.BiMonotoneComparison.exists_rectangle {X : Type u_1} {Y : Type u_2} (q : BiMonotoneComparison X Y) (A : Finset X) (B : Finset Y) (hA : A.Nonempty) (hB : B.Nonempty) {a : ℝ} (ha : 0 ≤ a) (ha₁ : a ≤ 1) : ∃ (b : Bool) (A' : Finset X) (B' : Finset Y), A' ⊆ A ∧ B' ⊆ B ∧ A'.Nonempty ∧ B'.Nonempty ∧ (if b = true then 1 - a else a) * ↑A.card ≤ ↑A'.card ∧ (if b = true then 1 - a else a) * ↑B.card ≤ ↑B'.card ∧ ∀ x ∈ A', ∀ y ∈ B', q.eval x y = b

Either the false branch retains proportion a on both sides, or the true branch retains proportion 1 - a on both sides. The selected sides are nonempty, including when scores tie.

structure Cslib.SeparableComparison (X : Type u_1) (Y : Type u_2) : Type (max u_1 u_2)

A comparison of the sum of two independent scores against a threshold.

• left : X → ℝ

  The left score.

• right : Y → ℝ

  The right score.

• threshold : ℝ

  Equality at this threshold takes the true branch.

noncomputable def Cslib.SeparableComparison.eval {X : Type u_1} {Y : Type u_2} (q : SeparableComparison X Y) (x : X) (y : Y) : Bool

The answer to a separable comparison.

noncomputable def Cslib.SeparableComparison.toBiMonotone {X : Type u_1} {Y : Type u_2} (q : SeparableComparison X Y) : BiMonotoneComparison X Y

Every separable comparison is a bi-monotone comparison with additive threshold kernel.

@[simp]

theorem Cslib.SeparableComparison.eval_toBiMonotone {X : Type u_1} {Y : Type u_2} (q : SeparableComparison X Y) (x : X) (y : Y) : q.toBiMonotone.eval x y = q.eval x y

theorem Cslib.SeparableComparison.exists_rectangle {X : Type u_1} {Y : Type u_2} (q : SeparableComparison X Y) (A : Finset X) (B : Finset Y) (hA : A.Nonempty) (hB : B.Nonempty) {a : ℝ} (ha : 0 ≤ a) (ha₁ : a ≤ 1) : ∃ (b : Bool) (A' : Finset X) (B' : Finset Y), A' ⊆ A ∧ B' ⊆ B ∧ A'.Nonempty ∧ B'.Nonempty ∧ (if b = true then 1 - a else a) * ↑A.card ≤ ↑A'.card ∧ (if b = true then 1 - a else a) * ↑B.card ≤ ↑B'.card ∧ ∀ x ∈ A', ∀ y ∈ B', q.eval x y = b

Either the false branch retains proportion a on both sides, or the true branch retains proportion 1 - a on both sides. The selected sides are nonempty, including when scores tie.

theorem Cslib.DecisionTree.exists_leaf_rectangle_biMonotone {X : Type u_1} {Y : Type u_2} {β : Type u_3} (t : DecisionTree (BiMonotoneComparison X Y) β) (A : Finset X) (B : Finset Y) (hA : A.Nonempty) (hB : B.Nonempty) : ∃ (A' : Finset X) (B' : Finset Y) (p : List Bool), A' ⊆ A ∧ B' ⊆ B ∧ A'.Nonempty ∧ B'.Nonempty ∧ A.card ≤ A'.card * t.leafCount ∧ B.card ≤ B'.card * t.leafCount ∧ ∀ x ∈ A', ∀ y ∈ B', (t.path fun (q : BiMonotoneComparison X Y) => q.eval x y) = p

A nonempty product domain contains a rectangle reaching one leaf of a bi-monotone comparison tree, with at most the leaf count lost from each side. The natural-number inequalities are the division-free form of |A'| ≥ |A| / L and |B'| ≥ |B| / L.

theorem Cslib.DecisionTree.card_mul_le_mul_leafCount_sq_biMonotone {X : Type u_1} {Y : Type u_2} {β : Type u_3} (t : DecisionTree (BiMonotoneComparison X Y) β) (A : Finset X) (B : Finset Y) (hA : A.Nonempty) (hB : B.Nonempty) {R : ℕ} (hR : ∀ A' ⊆ A, ∀ B' ⊆ B, ∀ (z : β), (∀ x ∈ A', ∀ y ∈ B', (t.eval fun (q : BiMonotoneComparison X Y) => q.eval x y) = z) → A'.card * B'.card ≤ R) : A.card * B.card ≤ R * t.leafCount ^ 2

A bound on monochromatic rectangle area forces a squared lower bound on the leaf count of a bi-monotone comparison tree. This is the division-free form of L ≥ √(|A| |B| / R).

theorem Cslib.DecisionTree.exists_leaf_rectangle {X : Type u_1} {Y : Type u_2} {β : Type u_3} (t : DecisionTree (SeparableComparison X Y) β) (A : Finset X) (B : Finset Y) (hA : A.Nonempty) (hB : B.Nonempty) : ∃ (A' : Finset X) (B' : Finset Y) (p : List Bool), A' ⊆ A ∧ B' ⊆ B ∧ A'.Nonempty ∧ B'.Nonempty ∧ A.card ≤ A'.card * t.leafCount ∧ B.card ≤ B'.card * t.leafCount ∧ ∀ x ∈ A', ∀ y ∈ B', (t.path fun (q : SeparableComparison X Y) => q.eval x y) = p

A nonempty product domain contains a rectangle reaching one leaf, with at most the leaf count lost from each side. The natural-number inequalities are the division-free form of |A'| ≥ |A| / L and |B'| ≥ |B| / L.

theorem Cslib.DecisionTree.card_mul_le_mul_leafCount_sq {X : Type u_1} {Y : Type u_2} {β : Type u_3} (t : DecisionTree (SeparableComparison X Y) β) (A : Finset X) (B : Finset Y) (hA : A.Nonempty) (hB : B.Nonempty) {R : ℕ} (hR : ∀ A' ⊆ A, ∀ B' ⊆ B, ∀ (z : β), (∀ x ∈ A', ∀ y ∈ B', (t.eval fun (q : SeparableComparison X Y) => q.eval x y) = z) → A'.card * B'.card ≤ R) : A.card * B.card ≤ R * t.leafCount ^ 2

A bound on monochromatic rectangle area forces a squared lower bound on the leaf count. This is the division-free form of L ≥ √(|A| |B| / R).