Section 12 pasting: Bernoulli tail polynomial combinatorics

Finset re-indexing and cardinality-grouping lemmas for the Bernoulli-tail operator endpoint of the fromHToG recurrence.

noncomputable def MIPStarRE.LDT.Pasting.gHatTypeFinsetEquiv (k : ℕ) : GHatType k ≃ Finset (Fin k)

Boolean type patterns are equivalent to their support finsets.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatTypeWeight_of_finset {k : ℕ} (s : Finset (Fin k)) : (gHatTypeWeight fun (i : Fin k) => decide (i ∈ s)) = s.card

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatTypeOperator_of_finset {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Quantum.Op ι) {k : ℕ} (s : Finset (Fin k)) : (gHatTypeOperator G fun (i : Fin k) => decide (i ∈ s)) = G ^ s.card * (1 - G) ^ (k - s.card)

theorem MIPStarRE.LDT.Pasting.fromHToG_truncatedTypeSums_full_as_finset_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Quantum.Op ι) (d k : ℕ) : truncatedTypeSums G d k default = ∑ s : Finset (Fin k), if d + 1 ≤ s.card then G ^ s.card * (1 - G) ^ (k - s.card) else 0

Rewrite the terminal truncated type sum as a sum over support finsets.

theorem MIPStarRE.LDT.Pasting.fromHToG_sum_finsets_by_card_indicator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Quantum.Op ι) (d k : ℕ) : (∑ s : Finset (Fin k), if d + 1 ≤ s.card then G ^ s.card * (1 - G) ^ (k - s.card) else 0) = ∑ r ∈ Finset.Icc (d + 1) k, ↑(k.choose r) • (G ^ r * (1 - G) ^ (k - r))

Group the terminal support-finset sum by cardinality, producing the binomial coefficients in the Bernoulli-tail polynomial. The key combinatorial step is Mathlib's Finset.sum_powerset_apply_card, applied to Finset.univ : Finset (Fin k).

theorem MIPStarRE.LDT.Pasting.fromHToG_truncatedTypeSums_full_eq_bernoulliTailOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Quantum.Op ι) (d k : ℕ) : truncatedTypeSums G d k default = bernoulliTailOperator k d G

Terminal endpoint of the recurrence weight: after all k bits have been converted, the truncated type sum is exactly the Bernoulli-tail polynomial F(G).

theorem MIPStarRE.LDT.Pasting.fromHToG_truncatedTypeSums_zero_eq_indicator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Quantum.Op ι) (d : ℕ) {tailLen : ℕ} (τtail : GHatType tailLen) : truncatedTypeSums G d 0 τtail = if d + 1 ≤ gHatTypeWeight τtail then 1 else 0

At prefix length zero, the recurrence weight is exactly the eligibility indicator for the remaining type: the empty prefix contributes the identity when |τtail| ≥ d + 1, and contributes zero otherwise.