ML.Partition­Predictor

Roll-up: finite-partition (piecewise-constant) predictors and their fixed-average ensembles, with the structural range-preservation property.

Finite­Partition­Predictor 3 core · 0 supporting A finite-partition predictor has 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

A finite-partition predictor has a finite set of cells, a map sending each input to its cell, and a value per cell. The predictor is piecewise constant on those cells.

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/PartitionPredictor/FinitePartitionPredictor.lean:21
def eval reviewed
Causalean.ML.FinitePartitionPredictor

A finite-partition prediction returns its cell's constant. It evaluates a finite-partition predictor on an input from its domain.

Definition (Lean source)
parameters
X :
Type*
T :
FinitePartitionPredictor X
x :
X
def
eval T x :
ℝ
given by
T.value (T.chooseCell x)
Causalean.ML.FinitePartitionPredictor.eval · Causalean/ML/PartitionPredictor/FinitePartitionPredictor.lean:36 · uses FinitePartitionPredictor
theorem eval_eqOn_cell reviewed
Causalean.ML.FinitePartitionPredictor

A finite-partition predictor is constant on each cell: the predictor returns the cell's assigned value throughout the inputs mapped 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/PartitionPredictor/FinitePartitionPredictor.lean:42 · uses FinitePartitionPredictor , eval
Ensemble 3 core · 0 supporting This file models a fixed-size finite ensemble of FinitePartitionPredictors over an input type X. ★ PartitionEnsemble★ eval_mem_Icc

Finite-partition predictor ensembles

This file models a fixed-size finite ensemble of FinitePartitionPredictors over an input type X. The public API consists of PartitionEnsemble, which stores one predictor for each index in Fin T, and PartitionEnsemble.eval, their uniform average.

The main structural theorem, PartitionEnsemble.eval_mem_Icc, states that a nonempty ensemble preserves pointwise interval bounds: if every member's value lies in [a, b] at every input, then the averaged value also lies in [a, b].

structure PartitionEnsemble reviewed
Causalean.ML

A finite-partition predictor ensemble: one predictor tree for each index in Fin T.

Definition (Lean source)
parameters
X :
Type*
T :
ℕ
fields
The ensemble members.
tree :
Fin T → FinitePartitionPredictor X
Causalean.ML.PartitionEnsemble · Causalean/ML/PartitionPredictor/Ensemble.lean:28
def eval reviewed
Causalean.ML.PartitionEnsemble

A finite-partition ensemble prediction is the memberwise average. It evaluates an ensemble with the specified member count at an input point in its domain.

Definition (Lean source)
parameters
X :
Type*
T :
ℕ
F :
PartitionEnsemble X T
x :
X
def
eval F x :
ℝ
given by
(T : ℝ)⁻¹ * ∑ t : Fin T, (F.tree t).eval x
Causalean.ML.PartitionEnsemble.eval · Causalean/ML/PartitionPredictor/Ensemble.lean:34 · uses PartitionEnsemble
theorem eval_mem_Icc reviewed
Causalean.ML.PartitionEnsemble

A nonempty ensemble average preserves common member bounds. For the ensemble and evaluation point, this follows from having at least one member and uniform memberwise bounds at every input.

Formal statement
hypotheses
X :
Type*
T :
ℕ
F :
PartitionEnsemble 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 PartitionEnsemble.eval_mem_Icc {X : Type*} {T : ℕ} (F : PartitionEnsemble 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 [PartitionEnsemble.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 [PartitionEnsemble.eval] using hscale _ = b := by field_simp [hTne]
Causalean.ML.PartitionEnsemble.eval_mem_Icc · Causalean/ML/PartitionPredictor/Ensemble.lean:42 · uses eval , PartitionEnsemble , eval