Documentation

MIPRE.Background.LIDT.Co.Pasting.Bernoulli.Weights

Section 12 pasting: Bernoulli recurrence weights #

Recurrence-weight identities for the fromHToG reduction: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Bernoulli/Weights.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The slice family is an IdxPolyFamily params 𝔓, so the recurrence weight fromHToGRecurrenceWeight params family prefixLen τtail and the averaged complete operator G = family.averagedSubMeas.total are local operators in 𝔓 (the vendored Op ι). Every fact here is truncatedTypeSumRecurrence or a commutation lemma of Co/Pasting/Bernoulli/TruncatedSums.lean at that G; the Hermitian statement is star W = W (the vendored Wᴴ = W).

Not ported #

Every declaration of the vendored file has a counterpart here.

References #

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

source
theorem MIPRE.LIDT.Co.Pasting.fromHToGRecurrenceWeight_recurrence {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) :
star (truncatedTypeSums family.averagedSubMeas.total params.d prefixLen τtail) = truncatedTypeSums family.averagedSubMeas.total params.d prefixLen τtail ∧ 0 ≤ truncatedTypeSums family.averagedSubMeas.total params.d prefixLen τtail ∧ truncatedTypeSums family.averagedSubMeas.total params.d prefixLen τtail ≤ 1 ∧ truncatedTypeSums family.averagedSubMeas.total params.d (prefixLen + 1) τtail = truncatedTypeSums family.averagedSubMeas.total params.d prefixLen (MIPStarRE.LDT.Pasting.prependTypeBit true τtail) * family.averagedSubMeas.total + truncatedTypeSums family.averagedSubMeas.total params.d prefixLen (MIPStarRE.LDT.Pasting.prependTypeBit false τtail) * (1 - family.averagedSubMeas.total)

Bundle the four proved facts about the averaged total operator G used by fromHToGRecurrenceWeight into a single truncatedTypeSumRecurrence call.

source
theorem MIPRE.LIDT.Co.Pasting.fromHToGRecurrenceWeight_isHermitian {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) :
star (fromHToGRecurrenceWeight params family prefixLen τtail) = fromHToGRecurrenceWeight params family prefixLen τtail

fromHToGRecurrenceWeight is self-adjoint (source-style API).

source
theorem MIPRE.LIDT.Co.Pasting.fromHToGRecurrenceWeight_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) :
0 ≤ fromHToGRecurrenceWeight params family prefixLen τtail

fromHToGRecurrenceWeight is positive (source-style API).

source
theorem MIPRE.LIDT.Co.Pasting.fromHToGRecurrenceWeight_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) :
fromHToGRecurrenceWeight params family prefixLen τtail ≤ 1

fromHToGRecurrenceWeight is bounded above by the identity.

source
theorem MIPRE.LIDT.Co.Pasting.fromHToGRecurrenceWeight_commute_base {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) :
Commute (fromHToGRecurrenceWeight params family prefixLen τtail) family.averagedSubMeas.total

fromHToGRecurrenceWeight commutes with the averaged complete operator G.

source
theorem MIPRE.LIDT.Co.Pasting.fromHToGRecurrenceWeight_commute_one_sub_base {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) :
Commute (fromHToGRecurrenceWeight params family prefixLen τtail) (1 - family.averagedSubMeas.total)

fromHToGRecurrenceWeight commutes with I - G.

source
theorem MIPRE.LIDT.Co.Pasting.fromHToGRecurrenceWeight_succ {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) :
fromHToGRecurrenceWeight params family (prefixLen + 1) τtail = fromHToGRecurrenceWeight params family prefixLen (MIPStarRE.LDT.Pasting.prependTypeBit true τtail) * family.averagedSubMeas.total + fromHToGRecurrenceWeight params family prefixLen (MIPStarRE.LDT.Pasting.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.