Documentation

MIPRE.Background.LIDT.Co.Pasting.Bernoulli.TruncatedSums

Section 12 pasting: Bernoulli truncated sums #

Truncated type sums and their one-step recurrence: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Bernoulli/TruncatedSums.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

No declaration of the vendored file reads a state. The algebraic identities (the one-bit recurrences of the type monomials, their commutation with G and 1 - G, the binomial expansion ∑_τ G^{|τ|} (1 - G)^{k - |τ|} = 1) hold in any ring, and the positivity facts in any C*-algebra with its order, through CStarAlgebra.pow_nonneg and Commute.mul_nonneg in place of the vendored Matrix.PosSemidef arguments, as in Co/Pasting/Sandwich/GHatSandwich.lean; so they serve the local algebra 𝔓 and K →L[ℂ] K alike. The Hermitian clause of truncatedTypeSumRecurrence is star T = T (the vendored Tᴴ = T), read off positivity.

The three type-weight identities of the vendored file are classical: this file imports the vendored file and names them through an explicit open MIPStarRE.LDT.Pasting (…) list.

Not ported #

References #

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

source
theorem MIPRE.LIDT.Co.Pasting.gHatTypeWeight_prepend_true {k : ℕ} (τ : MIPStarRE.LDT.Pasting.GHatType k) :
MIPStarRE.LDT.Pasting.gHatTypeWeight (MIPStarRE.LDT.Pasting.prependTypeBit true τ) = MIPStarRE.LDT.Pasting.gHatTypeWeight τ + 1

Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.

source
theorem MIPRE.LIDT.Co.Pasting.gHatTypeWeight_prepend_false {k : ℕ} (τ : MIPStarRE.LDT.Pasting.GHatType k) :
MIPStarRE.LDT.Pasting.gHatTypeWeight (MIPStarRE.LDT.Pasting.prependTypeBit false τ) = MIPStarRE.LDT.Pasting.gHatTypeWeight τ

Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.

source
theorem MIPRE.LIDT.Co.Pasting.gHatTypeWeight_le {k : ℕ} (τ : MIPStarRE.LDT.Pasting.GHatType k) :
MIPStarRE.LDT.Pasting.gHatTypeWeight τ ≤ k

Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.

Bernoulli recurrence weights #

source
theorem MIPRE.LIDT.Co.Pasting.gHatTypeOperator_prepend_true {R : Type u_1} [Ring R] (G : R) {k : ℕ} (τ : MIPStarRE.LDT.Pasting.GHatType k) :
gHatTypeOperator G (MIPStarRE.LDT.Pasting.prependTypeBit true τ) = gHatTypeOperator G τ * G

Prepending a true bit multiplies the type monomial by G.

source
theorem MIPRE.LIDT.Co.Pasting.gHatTypeOperator_prepend_false {R : Type u_1} [Ring R] (G : R) {k : ℕ} (τ : MIPStarRE.LDT.Pasting.GHatType k) :
gHatTypeOperator G (MIPStarRE.LDT.Pasting.prependTypeBit false τ) = gHatTypeOperator G τ * (1 - G)

Prepending a false bit multiplies the type monomial by 1 - G.

source
theorem MIPRE.LIDT.Co.Pasting.gHatTypeOperator_commute_base {R : Type u_1} [Ring R] (G : R) {k : ℕ} (τ : MIPStarRE.LDT.Pasting.GHatType k) :
Commute (gHatTypeOperator G τ) G

Each Boolean-type monomial commutes with the base operator G.

source
theorem MIPRE.LIDT.Co.Pasting.gHatTypeOperator_commute_one_sub_base {R : Type u_1} [Ring R] (G : R) {k : ℕ} (τ : MIPStarRE.LDT.Pasting.GHatType k) :
Commute (gHatTypeOperator G τ) (1 - G)

Each Boolean-type monomial commutes with the complementary base operator 1 - G.

source
theorem MIPRE.LIDT.Co.Pasting.truncatedTypeSums_commute_base {R : Type u_1} [Ring R] (G : R) (d prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) :
Commute (truncatedTypeSums G d prefixLen τtail) G

The truncated type sum commutes with the base operator G.

source
theorem MIPRE.LIDT.Co.Pasting.truncatedTypeSums_commute_one_sub_base {R : Type u_1} [Ring R] (G : R) (d prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) :
Commute (truncatedTypeSums G d prefixLen τtail) (1 - G)

The truncated type sum commutes with the complementary base operator 1 - G.

source
theorem MIPRE.LIDT.Co.Pasting.full_gHatType_sum_eq_one {R : Type u_1} [Ring R] (G : R) (prefixLen : ℕ) :
∑ τprefix : MIPStarRE.LDT.Pasting.GHatType prefixLen, gHatTypeOperator G τprefix = 1

The full sum of type operators equals the identity.

This is the commuting binomial expansion ∑ τ : GHatType k, G ^ |τ| * (1 - G) ^ (k - |τ|) = (G + (1 - G))^k = 1.

source
theorem MIPRE.LIDT.Co.Pasting.gHatTypeOperator_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (G : A) (hGpsd : 0 ≤ G) (hGleOne : G ≤ 1) {k : ℕ} (τ : MIPStarRE.LDT.Pasting.GHatType k) :
0 ≤ gHatTypeOperator G τ

Each type monomial of a positive contraction is positive.

source
theorem MIPRE.LIDT.Co.Pasting.truncatedTypeSumRecurrence {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (G : A) (hGpsd : 0 ≤ G) (hGleOne : G ≤ 1) (d prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) :
star (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 (MIPStarRE.LDT.Pasting.prependTypeBit true τtail) * G + truncatedTypeSums G d prefixLen (MIPStarRE.LDT.Pasting.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.