Boolean Mask Partition of Derivative Directions

This is a combinatorial lemma for the ordered selection operation selected.

For any type $E$, any $m\in\mathbb N$, any list of directions $h:\operatorname{Fin}(m)\to E$, and any Boolean mask $q:\operatorname{Fin}(m)\to\{\mathrm{false},\mathrm{true}\}$:

1. The lengths of the selected and complementary lists add to $m$.
2. Their concatenation is a permutation of List.ofFn h.
3. The mask selecting exactly one fixed index $i$ produces the singleton list $[h_i]$.
4. If selected h q has length $1$, then $q$ is the indicator of some single index.

The result is purely combinatorial and supports the subset bookkeeping in higher-order Leibniz expansions.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem selected_mask_partition {E : Type*} {m : ℕ}
    (h : Fin m → E) (q : Fin m → Bool) :
    (selected h q).length + (selected h (fun i => !(q i))).length = m ∧
    (selected h q ++ selected h (fun i => !(q i))).Perm (List.ofFn h) ∧
    (∀ i : Fin m, selected h (fun j => decide (j = i)) = [h i]) ∧
    ((selected h q).length = 1 → ∃ i : Fin m, q = fun j => decide (j = i))

Module navigation

Module: Analysis/IteratedDerivative/Bilinear.

Previous: sum_filter_eq_two_mul_sum_filter_of_compl_invariant.

Source excerpt, lines 177–182 · Frozen source 408915f.