ML.Tree

Roll-up: finite-partition (piecewise-constant) tree predictors and random-forest averaging, with the structural range-preservation property.

Finite­Partition­Predictor 3 core · 0 supporting A regression tree, abstracted to its essential structure: a finite set of cells, a map sending each input to its cell, and a value per cell. ★ FinitePartitionPredictor★ eval_eqOn_cell

Finite-partition predictors (regression trees)

A regression tree, abstracted to its essential structure: a finite set of cells, a map sending each input to its cell, and a value per cell. The predictor is piecewise constant on the cells. (CART greediness, splits, and bootstrap are out of scope; this is the structural target a tree compiles to.)

structure FinitePartitionPredictor reviewed
Causalean.ML

A piecewise-constant predictor on a finite partition: a finite index type cell of partition cells, a map chooseCell assigning each input to its cell, and a constant predicted value value on each cell.

Definition (Lean source)
parameters
X :
Type*
fields
The (finite) index type of partition cells.
cell :
Type
Finiteness of the cell index.
fintypeCell :
Fintype cell
The cell that an input falls into.
chooseCell :
X → cell
The constant predicted value on each cell.
value :
cell → ℝ
Causalean.ML.FinitePartitionPredictor · Causalean/ML/Tree/FinitePartitionPredictor.lean:18
def eval reviewed
Causalean.ML.FinitePartitionPredictor

The tree prediction: the value of the cell the input falls into.

Definition (Lean source)
def FinitePartitionPredictor.eval {X : Type*} (T : FinitePartitionPredictor X) (x : X) : ℝ := T.value (T.chooseCell x)
Causalean.ML.FinitePartitionPredictor.eval · Causalean/ML/Tree/FinitePartitionPredictor.lean:33 · uses FinitePartitionPredictor
theorem eval_eqOn_cell reviewed
Causalean.ML.FinitePartitionPredictor

For a finite-partition predictor T, on the set of inputs mapped to a given cell c, the predictor's output equals the constant value assigned to that cell.

Formal statement
hypotheses
X :
Type*
T :
FinitePartitionPredictor X
c :
T.cell
conclusion
EqOn T.eval (fun _ => T.value c) {x | T.chooseCell x = c}
Proof (Lean source)
theorem FinitePartitionPredictor.eval_eqOn_cell {X : Type*} (T : FinitePartitionPredictor X) (c : T.cell) : EqOn T.eval (fun _ => T.value c) {x | T.chooseCell x = c} := by intro x hx simp only [FinitePartitionPredictor.eval, Set.mem_setOf_eq] at hx ⊢ rw [hx]
Causalean.ML.FinitePartitionPredictor.eval_eqOn_cell · Causalean/ML/Tree/FinitePartitionPredictor.lean:37 · uses FinitePartitionPredictor , eval
Forest 3 core · 0 supporting This file models a random forest as a fixed-size finite ensemble of FinitePartitionPredictors over an input type X. ★ RandomForest★ eval_mem_Icc

Random forests

This file models a random forest as a fixed-size finite ensemble of FinitePartitionPredictors over an input type X. The public API consists of RandomForest, which stores one tree for each index in Fin T, and RandomForest.eval, the uniform average of the tree predictions.

The main structural theorem, RandomForest.eval_mem_Icc, states that a nonempty forest preserves pointwise interval bounds: if every tree prediction lies in [a, b] at every input, then the averaged forest prediction also lies in [a, b].

structure RandomForest reviewed
Causalean.ML

A random forest: one finite-partition regression tree tree for each index in Fin T.

Definition (Lean source)
parameters
X :
Type*
T :
ℕ
fields
The ensemble of trees.
tree :
Fin T → FinitePartitionPredictor X
Causalean.ML.RandomForest · Causalean/ML/Tree/Forest.lean:25
def eval reviewed
Causalean.ML.RandomForest

The forest prediction: the average of the tree predictions.

Definition (Lean source)
noncomputable def RandomForest.eval {X : Type*} {T : ℕ} (F : RandomForest X T) (x : X) : ℝ := (T : ℝ)⁻¹ * ∑ t : Fin T, (F.tree t).eval x
Causalean.ML.RandomForest.eval · Causalean/ML/Tree/Forest.lean:31 · uses RandomForest
theorem eval_mem_Icc reviewed
Causalean.ML.RandomForest

For a random forest F of T finite-partition regression trees, if the forest is nonempty (T > 0) and every tree predicts within [a, b] at every input, then the forest's averaged prediction also lies in [a, b] at every input x.

Formal statement
hypotheses
X :
Type*
T :
ℕ
F :
RandomForest X T
hT :
0 < T
a b :
ℝ
hb :
∀ (t : Fin T) (x : X), (F.tree t).eval x ∈ Icc a b
x :
X
conclusion
F.eval x ∈ Icc a b
Proof (Lean source)
theorem RandomForest.eval_mem_Icc {X : Type*} {T : ℕ} (F : RandomForest X T) (hT : 0 < T) {a b : ℝ} (hb : ∀ (t : Fin T) (x : X), (F.tree t).eval x ∈ Icc a b) (x : X) : F.eval x ∈ Icc a b := by rw [Set.mem_Icc] have hTpos : 0 < (T : ℝ) := Nat.cast_pos.mpr hT have hTne : (T : ℝ) ≠ 0 := ne_of_gt hTpos have hsum_lower : (T : ℝ) * a ≤ ∑ t : Fin T, (F.tree t).eval x := by calc (T : ℝ) * a = ∑ _t : Fin T, a := by simp [Finset.sum_const, nsmul_eq_mul] _ ≤ ∑ t : Fin T, (F.tree t).eval x := by exact Finset.sum_le_sum (fun t _ => (Set.mem_Icc.mp (hb t x)).1) have hsum_upper : ∑ t : Fin T, (F.tree t).eval x ≤ (T : ℝ) * b := by calc ∑ t : Fin T, (F.tree t).eval x ≤ ∑ _t : Fin T, b := by exact Finset.sum_le_sum (fun t _ => (Set.mem_Icc.mp (hb t x)).2) _ = (T : ℝ) * b := by simp [Finset.sum_const, nsmul_eq_mul] constructor · have hscale := mul_le_mul_of_nonneg_left hsum_lower (inv_nonneg.mpr (le_of_lt hTpos)) calc a = (T : ℝ)⁻¹ * ((T : ℝ) * a) := by field_simp [hTne] _ ≤ F.eval x := by simpa [RandomForest.eval] using hscale · have hscale := mul_le_mul_of_nonneg_left hsum_upper (inv_nonneg.mpr (le_of_lt hTpos)) calc F.eval x ≤ (T : ℝ)⁻¹ * ((T : ℝ) * b) := by simpa [RandomForest.eval] using hscale _ = b := by field_simp [hTne]
Causalean.ML.RandomForest.eval_mem_Icc · Causalean/ML/Tree/Forest.lean:35 · uses eval , RandomForest , eval