Complement Pairing of Boolean Mask Sums

This is a finite-sum pairing identity for Boolean masks.

Let $P$ be a predicate on masks $q:\operatorname{Fin}(m)\to\{\mathrm{false},\mathrm{true}\}$, assume $P(q)$ is equivalent to $P(\neg q)$, and let $f$ assign a real number to each mask with $f(\neg q)=f(q)$. For any fixed $i_0\in\operatorname{Fin}(m)$,

The identity pairs every mask with its complement and is used to restrict symmetric subset sums to representatives containing a chosen slot.

Original Lean declaration header

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

theorem sum_filter_eq_two_mul_sum_filter_of_compl_invariant {m : ℕ} (P : (Fin m → Bool) → Prop)
    [DecidablePred P] (hP : ∀ q, P (fun i => !(q i)) ↔ P q) (f : (Fin m → Bool) → ℝ)
    (hf : ∀ q, f (fun i => !(q i)) = f q) (i₀ : Fin m) :
    ∑ q ∈ Finset.univ.filter P, f q = 2 * ∑ q ∈ Finset.univ.filter (fun q => q i₀ = true ∧ P q), f q

Module navigation

Module: Analysis/IteratedDerivative/Bilinear.

Previous: directional_bilinear · Next: selected_mask_partition.

Source excerpt, lines 119–122 · Frozen source 408915f.