Block sensitivity and exact decision trees

Disjoint sensitive blocks require distinct queries along the input's path. Induction removes at most one block at each queried coordinate. Querying every coordinate also supplies an exact tree of depth at most the input arity.

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivity_eval_le_depth {n : ℕ} (tree : DecisionTree.On n) : (blockSensitivity fun (x : Fin n → Bool) => DecisionTree.On.eval x tree) ≤ tree.depth

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.exists_decisionTree {n : ℕ} (f : BitString n → Bool) : ∃ (tree : DecisionTree.On n), (∀ (x : BitString n), DecisionTree.On.eval x tree = f x) ∧ tree.depth ≤ n

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivity_le_depth {n : ℕ} (f : BitString n → Bool) (tree : DecisionTree.On n) (heval : ∀ (x : BitString n), DecisionTree.On.eval x tree = f x) : blockSensitivity f ≤ tree.depth

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivityAt_le_blockSensitivityAt {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) : sensitivityAt f x ≤ blockSensitivityAt f x

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivity_le_blockSensitivity {I : Type} [Fintype I] (f : (I → Bool) → Bool) : sensitivity f ≤ blockSensitivity f

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivity_le_arity {n : ℕ} (f : BitString n → Bool) : blockSensitivity f ≤ n