Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.Pasting.Bernoulli.Weights

Section 12 pasting: Bernoulli recurrence weights #

Recurrence-weight identities for the fromHToG reduction.

source
theorem MIPStarRE.LDT.Pasting.fromHToGRecurrenceWeight_isHermitian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (prefixLen : ℕ) {tailLen : ℕ} (τtail : GHatType tailLen) :
Matrix.conjTranspose (fromHToGRecurrenceWeight params family prefixLen τtail) = fromHToGRecurrenceWeight params family prefixLen τtail

fromHToGRecurrenceWeight is Hermitian (source-style API).

source
theorem MIPStarRE.LDT.Pasting.fromHToGRecurrenceWeight_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (prefixLen : ℕ) {tailLen : ℕ} (τtail : GHatType tailLen) :
0 ≤ fromHToGRecurrenceWeight params family prefixLen τtail

fromHToGRecurrenceWeight is positive semidefinite (source-style API).

source
theorem MIPStarRE.LDT.Pasting.fromHToGRecurrenceWeight_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (prefixLen : ℕ) {tailLen : ℕ} (τtail : GHatType tailLen) :
fromHToGRecurrenceWeight params family prefixLen τtail ≤ 1

fromHToGRecurrenceWeight is bounded above by the identity.

source
theorem MIPStarRE.LDT.Pasting.fromHToGRecurrenceWeight_commute_base {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (prefixLen : ℕ) {tailLen : ℕ} (τtail : GHatType tailLen) :
Commute (fromHToGRecurrenceWeight params family prefixLen τtail) family.averagedSubMeas.total

fromHToGRecurrenceWeight commutes with the averaged complete operator G.

source
theorem MIPStarRE.LDT.Pasting.fromHToGRecurrenceWeight_commute_one_sub_base {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (prefixLen : ℕ) {tailLen : ℕ} (τtail : GHatType tailLen) :
Commute (fromHToGRecurrenceWeight params family prefixLen τtail) (1 - family.averagedSubMeas.total)

fromHToGRecurrenceWeight commutes with I - G.

source
theorem MIPStarRE.LDT.Pasting.fromHToGRecurrenceWeight_succ {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (prefixLen : ℕ) {tailLen : ℕ} (τtail : GHatType tailLen) :
fromHToGRecurrenceWeight params family (prefixLen + 1) τtail = fromHToGRecurrenceWeight params family prefixLen (prependTypeBit true τtail) * family.averagedSubMeas.total + fromHToGRecurrenceWeight params family prefixLen (prependTypeBit false τtail) * (1 - family.averagedSubMeas.total)

One-step recurrence for fromHToGRecurrenceWeight: adding a new prefix bit splits the weight into the τ_ℓ = 1 and τ_ℓ = 0 branches, each multiplied by the appropriate Bernoulli factor G or I - G.