Section 12 pasting: Bernoulli truncated sums #
Truncated type sums and their one-step recurrence.
Bernoulli recurrence weights #
theorem
MIPStarRE.LDT.Pasting.gHatTypeOperator_commute_base
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(G : Quantum.Op ι)
{k : ℕ}
(τ : GHatType k)
:
Commute (gHatTypeOperator G τ) G
Each Boolean-type monomial commutes with the base operator G.
theorem
MIPStarRE.LDT.Pasting.gHatTypeOperator_commute_one_sub_base
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(G : Quantum.Op ι)
{k : ℕ}
(τ : GHatType k)
:
Commute (gHatTypeOperator G τ) (1 - G)
Each Boolean-type monomial commutes with the complementary base operator 1 - G.
theorem
MIPStarRE.LDT.Pasting.truncatedTypeSums_commute_base
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(G : Quantum.Op ι)
(d prefixLen : ℕ)
{tailLen : ℕ}
(τtail : GHatType tailLen)
:
Commute (truncatedTypeSums G d prefixLen τtail) G
The truncated type sum commutes with the base operator G.
theorem
MIPStarRE.LDT.Pasting.truncatedTypeSums_commute_one_sub_base
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(G : Quantum.Op ι)
(d prefixLen : ℕ)
{tailLen : ℕ}
(τtail : GHatType tailLen)
:
Commute (truncatedTypeSums G d prefixLen τtail) (1 - G)
The truncated type sum commutes with the complementary base operator 1 - G.
theorem
MIPStarRE.LDT.Pasting.truncatedTypeSumRecurrence
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(G : Quantum.Op ι)
(hGpsd : 0 ≤ G)
(hGleOne : G ≤ 1)
(d prefixLen : ℕ)
{tailLen : ℕ}
(τtail : GHatType tailLen)
:
Matrix.conjTranspose (truncatedTypeSums G d prefixLen τtail) = truncatedTypeSums G d prefixLen τtail ∧ 0 ≤ truncatedTypeSums G d prefixLen τtail ∧ truncatedTypeSums G d prefixLen τtail ≤ 1 ∧ truncatedTypeSums G d (prefixLen + 1) τtail = truncatedTypeSums G d prefixLen (prependTypeBit true τtail) * G + truncatedTypeSums G d prefixLen (prependTypeBit false τtail) * (1 - G)
lem:truncated-type-sum-recurrence.
This records the Hermitian, positivity, boundedness, and one-step recurrence
properties of the truncated type sums used in the fromHToG reduction.