Section 12 — Definitions: tuples and operators

Tuple distributions, type abbreviations, and basic operator helpers.

def MIPStarRE.LDT.Pasting.distinctTuples (params : Parameters) (k : ℕ) : Set (PointTuple params k)

The set of k-tuples with distinct coordinates.

Equations

• MIPStarRE.LDT.Pasting.distinctTuples params k = {xs : MIPStarRE.LDT.PointTuple params k | Function.Injective xs}

noncomputable def MIPStarRE.LDT.Pasting.distinctTupleSupport (params : Parameters) (k : ℕ) : Finset (PointTuple params k)

The finite support of the distinct-tuple distribution.

Equations

• MIPStarRE.LDT.Pasting.distinctTupleSupport params k = {xs : MIPStarRE.LDT.PointTuple params k | Function.Injective xs}

@[simp]

theorem MIPStarRE.LDT.Pasting.mem_distinctTupleSupport (params : Parameters) (k : ℕ) (xs : PointTuple params k) : xs ∈ distinctTupleSupport params k ↔ Function.Injective xs

theorem MIPStarRE.LDT.Pasting.distinctTupleSupport_card (params : Parameters) (k : ℕ) : (distinctTupleSupport params k).card = params.q.descFactorial k

The number of injective k-tuples is the falling factorial q(q-1) ... (q-k+1).

theorem MIPStarRE.LDT.Pasting.distinctTupleSupport_nonempty_of_le (params : Parameters) (k : ℕ) (hk : k ≤ params.q) : (distinctTupleSupport params k).Nonempty

If k ≤ q, there exists an injective k-tuple.

theorem MIPStarRE.LDT.Pasting.distinctTupleSupport_eq_empty_of_lt (params : Parameters) (k : ℕ) (hk : params.q < k) : distinctTupleSupport params k = ∅

If q < k, no injective k-tuple of field elements exists.

noncomputable def MIPStarRE.LDT.Pasting.distinctTupleDistribution (params : Parameters) (k : ℕ) : Distribution (PointTuple params k)

Uniform distribution on pairwise-distinct k-tuples from Fq. Support is the set of injective functions Fin k → Fq params; weight is uniform 1 / |support| on support, 0 outside.

Equations

• MIPStarRE.LDT.Pasting.distinctTupleDistribution params k = MIPStarRE.LDT.Distribution.uniformOnFinset (MIPStarRE.LDT.Pasting.distinctTupleSupport params k)

@[simp]

theorem MIPStarRE.LDT.Pasting.distinctTupleDistribution_support (params : Parameters) (k : ℕ) : (distinctTupleDistribution params k).support = distinctTupleSupport params k

theorem MIPStarRE.LDT.Pasting.distinctTupleDistribution_weight (params : Parameters) (k : ℕ) (xs : PointTuple params k) : (distinctTupleDistribution params k).weight xs = if xs ∈ distinctTupleSupport params k then 1 / ↑(distinctTupleSupport params k).card else 0

The distinct-tuple distribution has the uniform weight on its finite support.

theorem MIPStarRE.LDT.Pasting.distinctTupleDistribution_weight_sum_le_one (params : Parameters) (k : ℕ) : ∑ xs ∈ (distinctTupleDistribution params k).support, (distinctTupleDistribution params k).weight xs ≤ 1

The distinct-tuple distribution has total mass at most 1.

theorem MIPStarRE.LDT.Pasting.distinctTupleDistribution_isProbability_of_le (params : Parameters) (k : ℕ) (hk : k ≤ params.q) : (distinctTupleDistribution params k).IsProbability

For k ≤ q, the distinct-tuple distribution is a probability distribution.

theorem MIPStarRE.LDT.Pasting.distinctTupleDistribution_toPMF_of_le (params : Parameters) (k : ℕ) (hk : k ≤ params.q) : (distinctTupleDistribution params k).toPMF ⋯ = PMF.uniformOfFinset (distinctTupleSupport params k) ⋯

For k ≤ q, the distinct-tuple distribution is Mathlib's uniform PMF on the finite support of injective tuples.

theorem MIPStarRE.LDT.Pasting.distinctTupleDistribution_weight_sum_eq_one_of_le (params : Parameters) (k : ℕ) (hk : k ≤ params.q) : ∑ xs ∈ (distinctTupleDistribution params k).support, (distinctTupleDistribution params k).weight xs = 1

For k ≤ q, the weights of the distinct-tuple distribution sum to one.

@[reducible, inline]

abbrev MIPStarRE.LDT.Pasting.GHatOutcome (params : Parameters) [FieldModel params.q] : Type u_2

The outcome type of the completed family \widehat G.

Equations

• MIPStarRE.LDT.Pasting.GHatOutcome params = Option (MIPStarRE.LDT.Polynomial params)

@[reducible, inline]

abbrev MIPStarRE.LDT.Pasting.SliceQuestion (params : Parameters) : Type

The question type for a single slice height.

Equations

• MIPStarRE.LDT.Pasting.SliceQuestion params = MIPStarRE.LDT.Fq params

@[reducible, inline]

abbrev MIPStarRE.LDT.Pasting.SlicePairQuestion (params : Parameters) : Type

The question type for an ordered pair of slice heights.

Equations

• MIPStarRE.LDT.Pasting.SlicePairQuestion params = (MIPStarRE.LDT.Fq params × MIPStarRE.LDT.Fq params)

@[reducible, inline]

abbrev MIPStarRE.LDT.Pasting.GHatTupleOutcome (params : Parameters) [FieldModel params.q] (k : ℕ) : Type u_2

The outcome type of a k-tuple of completed-slice answers.

Equations

• MIPStarRE.LDT.Pasting.GHatTupleOutcome params k = (Fin k → MIPStarRE.LDT.Pasting.GHatOutcome params)

@[reducible, inline]

abbrev MIPStarRE.LDT.Pasting.GHatType (k : ℕ) : Type

A Boolean type pattern for a completed-slice tuple.

Equations

• MIPStarRE.LDT.Pasting.GHatType k = (Fin k → Bool)

@[reducible, inline]

abbrev MIPStarRE.LDT.Pasting.SandwichedLineQuestion (params : Parameters) (k : ℕ) : Type

A sandwiched-line question consists of a point and a k-tuple of slice heights.

Equations

• MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k = (MIPStarRE.LDT.Point params × MIPStarRE.LDT.PointTuple params k)

@[reducible, inline]

abbrev MIPStarRE.LDT.Pasting.VerticalLineQuestion (params : Parameters) : Type

The question type for vertical lines, identified with their base point.

Equations

• MIPStarRE.LDT.Pasting.VerticalLineQuestion params = MIPStarRE.LDT.Point params

def MIPStarRE.LDT.Pasting.gHatTypeWeight {k : ℕ} (τ : GHatType k) : ℕ

The Hamming weight |τ| of a type τ ∈ {0,1}^k.

Equations

• MIPStarRE.LDT.Pasting.gHatTypeWeight τ = {i : Fin k | τ i = true}.card

def MIPStarRE.LDT.Pasting.prependTypeBit {k : ℕ} (b : Bool) (τ : GHatType k) : GHatType (k + 1)

Prepend one type bit to a tail type.

Equations

• MIPStarRE.LDT.Pasting.prependTypeBit b τ = Fin.cons b τ

noncomputable def MIPStarRE.LDT.Pasting.gHatTypeOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Quantum.Op ι) {k : ℕ} (τ : GHatType k) : Quantum.Op ι

The operator monomial associated with a type τ.

Equations

• MIPStarRE.LDT.Pasting.gHatTypeOperator G τ = G ^ MIPStarRE.LDT.Pasting.gHatTypeWeight τ * (1 - G) ^ (k - MIPStarRE.LDT.Pasting.gHatTypeWeight τ)

noncomputable def MIPStarRE.LDT.Pasting.truncatedTypeSums {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Quantum.Op ι) (d prefixLen : ℕ) {tailLen : ℕ} (τtail : GHatType tailLen) : Quantum.Op ι

def:truncated-type-sums.

Fixing a tail type τ_tail, this sums the source-style monomials contributed by all prefixes whose total Hamming weight can still reach the interpolation threshold d + 1. The parameter prefixLen is the paper's ℓ - 1.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.bernoulliTailOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (k degree : ℕ) (X : Quantum.Op ι) : Quantum.Op ι

The Bernoulli tail operator from lem:chernoff-bernoulli-matrix: F(X) = ∑_{r=degree+1}^{k} C(k,r) · X^r · (I - X)^{k-r}. This is the matrix-valued Bernoulli tail probability.

Equations

• MIPStarRE.LDT.Pasting.bernoulliTailOperator k degree X = ∑ r ∈ Finset.Icc (degree + 1) k, ↑(k.choose r) • (X ^ r * (1 - X) ^ (k - r))

theorem MIPStarRE.LDT.Pasting.bernoulliTailOperator_leftTensor {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Quantum.Op ι) (k degree : ℕ) : bernoulliTailOperator k degree (leftTensor A) = leftTensor (bernoulliTailOperator k degree A)

The Bernoulli-tail polynomial commutes with left tensor placement.

noncomputable def MIPStarRE.LDT.Pasting.multiplyByTotalOnRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) : OpFamily α ι

Multiply each outcome operator by a total operator on the right.

Equations

• MIPStarRE.LDT.Pasting.multiplyByTotalOnRight A B = { outcome := fun (a : α) => A.outcome a * B.total, total := A.total * B.total }

noncomputable def MIPStarRE.LDT.Pasting.multiplyByTotalOnLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) : OpFamily β ι

Multiply each outcome operator by a total operator on the left.

Equations

• MIPStarRE.LDT.Pasting.multiplyByTotalOnLeft A B = { outcome := fun (b : β) => A.total * B.outcome b, total := A.total * B.total }

def MIPStarRE.LDT.Pasting.gHatTupleType {params : Parameters} {k : ℕ} [FieldModel params.q] (gs : GHatTupleOutcome params k) : GHatType k

Record which completed-slice outcomes are genuine polynomial outcomes.

Equations

• MIPStarRE.LDT.Pasting.gHatTupleType gs i = Option.isSome (gs i)

def MIPStarRE.LDT.Pasting.gHatTupleSupport {params : Parameters} {k : ℕ} [FieldModel params.q] (gs : GHatTupleOutcome params k) : Finset (Fin k)

The support of a completed-slice tuple, i.e. the indices whose outcomes are genuine polynomials rather than ⊥. This matches the paper's support of the type τ ∈ {0,1}^k.

Equations

• MIPStarRE.LDT.Pasting.gHatTupleSupport gs = {i : Fin k | Option.isSome (gs i) = true}

def MIPStarRE.LDT.Pasting.gHatTupleHammingWeight {params : Parameters} {k : ℕ} [FieldModel params.q] (gs : GHatTupleOutcome params k) : ℕ

The Hamming weight of a completed-slice tuple.

Equations

• MIPStarRE.LDT.Pasting.gHatTupleHammingWeight gs = (MIPStarRE.LDT.Pasting.gHatTupleSupport gs).card

def MIPStarRE.LDT.Pasting.outcomesByType {params : Parameters} {k : ℕ} [FieldModel params.q] (τ : GHatType k) : Set (GHatTupleOutcome params k)

The set \mathsf{Outcomes}_\tau of completed-slice tuples whose Some/none pattern is prescribed by the type τ.

Equations

• MIPStarRE.LDT.Pasting.outcomesByType τ = {gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params k | ∀ (i : Fin k), Option.isSome (gs i) = τ i}

def MIPStarRE.LDT.Pasting.InterpolationEligible (params : Parameters) {k : ℕ} [FieldModel params.q] (gs : GHatTupleOutcome params k) : Prop

A completed-slice tuple is eligible for interpolation exactly when its type has Hamming weight at least d + 1, matching the paper's |w| ≥ d+1 filter.

Equations

• MIPStarRE.LDT.Pasting.InterpolationEligible params gs = (params.d + 1 ≤ MIPStarRE.LDT.Pasting.gHatTupleHammingWeight gs)