Splitting off the newly inserted coordinate #
The old signed-exponential state law is exactly the common law obtained in the enlarged system after deleting its last coordinate. Consequently, the lower and upper enlarged states are respectively the positive and negative exponential shifts of the old law. These are the dimension-change identifications used at every chain-insertion edge.
theorem
Feige.stateFactorList_castSucc_perm
{n : ℕ}
(γ β : Fin (n + 1) → ℝ)
(hγ : ∀ (i : Fin (n + 1)), 0 < γ i)
(hβ : ∀ (i : Fin (n + 1)), 0 < β i)
(S : Finset (Fin n))
:
(List.map (LikelihoodRatio.stateFactor (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) ⋯ ⋯ S)
Finset.univ.toList).Perm
(List.map (LikelihoodRatio.stateFactor γ β hγ hβ (liftChainState S)) (Finset.univ.erase (Fin.last n)).toList)
The complete list of signed factors on Fin n, embedded by
Fin.castSucc, is a permutation of the enlarged factor list with the last
coordinate erased.
theorem
Feige.insertionCommonLaw_last_eq_stateLaw
{n : ℕ}
(γ β : Fin (n + 1) → ℝ)
(hγ : ∀ (i : Fin (n + 1)), 0 < γ i)
(hβ : ∀ (i : Fin (n + 1)), 0 < β i)
(S : Finset (Fin n))
:
insertionCommonLaw γ β hγ hβ (liftChainState S) (Fin.last n) = stateLaw (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) S
Removing the newly inserted last coordinate from the enlarged common
law leaves precisely the old n-coordinate state law.
theorem
Feige.stateLaw_liftChainState_eq_zPlus_old
{n : ℕ}
(γ β : Fin (n + 1) → ℝ)
(hγ : ∀ (i : Fin (n + 1)), 0 < γ i)
(hβ : ∀ (i : Fin (n + 1)), 0 < β i)
(S : Finset (Fin n))
:
stateLaw γ β (liftChainState S) = TransferStein.zPlusLaw (stateLaw (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) S)
(γ (Fin.last n))
At a lifted lower state, the last coordinate contributes the positive
shift γ_last E.