Realizing the genuine edges of an insertion chain #
At every old chain level, the three numerical sequences F, B, and A
are respectively the nonnegative-tail probability of the old state law,
the positive shift by the new low-side scale, and the negative shift by the
new high-side scale. This identifies every nonterminal edge with the
finite signed-exponential instance of the local transfer step.
theorem
Feige.insertionOldK_eq_F_stateLaw
{n : ℕ}
(γ β : Fin (n + 1) → ℝ)
(σ : Equiv.Perm (Fin n))
(r : Fin (n + 1))
:
insertionOldK γ β σ ↑r = Lemma43.F (stateLaw (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) (chainState σ r))
theorem
Feige.insertionLowerK_eq_B_stateLaw
{n : ℕ}
(γ β : Fin (n + 1) → ℝ)
(hγ : ∀ (i : Fin (n + 1)), 0 < γ i)
(hβ : ∀ (i : Fin (n + 1)), 0 < β i)
(σ : Equiv.Perm (Fin n))
(r : Fin (n + 1))
:
insertionLowerK γ β σ ↑r = Lemma43.B (stateLaw (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) (chainState σ r))
(γ (Fin.last n))
theorem
Feige.insertionUpperK_eq_A_stateLaw
{n : ℕ}
(γ β : Fin (n + 1) → ℝ)
(hγ : ∀ (i : Fin (n + 1)), 0 < γ i)
(hβ : ∀ (i : Fin (n + 1)), 0 < β i)
(σ : Equiv.Perm (Fin n))
(r : Fin (n + 1))
:
insertionUpperK γ β σ ↑r = Lemma43.A (stateLaw (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) (chainState σ r))
(β (Fin.last n))
theorem
Feige.insertionTheta_eq_theta_stateLaw
{n : ℕ}
(γ β : Fin (n + 1) → ℝ)
(hγ : ∀ (i : Fin (n + 1)), 0 < γ i)
(hβ : ∀ (i : Fin (n + 1)), 0 < β i)
(σ : Equiv.Perm (Fin n))
(r : Fin (n + 1))
:
insertionTheta γ β σ ↑r = Lemma43.theta (stateLaw (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) (chainState σ r))
(γ (Fin.last n)) (β (Fin.last n))
theorem
Feige.realizesInsertionEdge_interior
{n : ℕ}
(γ β : Fin (n + 1) → ℝ)
(hγ : ∀ (i : Fin (n + 1)), 0 < γ i)
(hβ : ∀ (i : Fin (n + 1)), 0 < β i)
(σ : Equiv.Perm (Fin n))
(j : Fin n)
:
Lemma43.RealizesInsertionEdge (insertionUpperK γ β σ) (insertionOldK γ β σ) (insertionWidth γ β σ)
(insertionTheta γ β σ) (↑j)
(TransferStein.zPlusLaw
(MeasureTheory.volume.withDensity
(LikelihoodRatio.finiteSignedExpSumDensity
(LikelihoodRatio.commonFactors (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) ⋯ ⋯
(chainState σ j.castSucc) (σ j))))
(γ (σ j).castSucc))
(TransferStein.zMinusLaw
(MeasureTheory.volume.withDensity
(LikelihoodRatio.finiteSignedExpSumDensity
(LikelihoodRatio.commonFactors (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) ⋯ ⋯
(chainState σ j.castSucc) (σ j))))
(β (σ j).castSucc))
(γ (Fin.last n)) (β (Fin.last n))
Every genuine adjacent pair of old chain levels realizes exactly the finite signed-exponential endpoint pair consumed by the local transfer step.