The local transfer result in the insertion-sequence interface

The analytic transfer statement is phrased in terms of two probability laws, while the chain-insertion step consumes four numerical sequences along an old Boolean chain. This file records the exact, purely algebraic interface between those two presentations.

theorem Feige.Lemma43.theta_nonneg (ν : MeasureTheory.Measure ℝ) (c d : ℝ) : 0 ≤ theta ν c d

def Feige.Lemma43.RealizesInsertionEdge (upper old width interpolation : ℕ → ℝ) (j : ℕ) (νP νM : MeasureTheory.Measure ℝ) (c d : ℝ) : Prop

The entries of the insertion sequences at one edge are represented by the two laws occurring in the local transfer step.

Equations

• One or more equations did not get rendered due to their size.

theorem Feige.Lemma43.insertionTransfer_eq_of_realizesInsertionEdge {upper old width interpolation : ℕ → ℝ} {j : ℕ} {νP νM : MeasureTheory.Measure ℝ} {a c d : ℝ} (hreal : RealizesInsertionEdge upper old width interpolation j νP νM c d) (hid : (1 - theta νM c d) * (A νP d - A νM d) - c / (c + d) * (F νP - F νM) = (a - c) / (c + d) * w νP c d * (theta νP c d - theta νM c d)) : insertionTransfer upper old interpolation (c / (c + d)) j = (a - c) / (c + d) * width j * (interpolation j - interpolation (j + 1))

The factorized local transfer identity is exactly the identity required on one chain-insertion edge.

theorem Feige.Lemma43.insertion_order_widths_of_realizesInsertionEdge {upper old width interpolation : ℕ → ℝ} {j : ℕ} {νP νM : MeasureTheory.Measure ℝ} {c d : ℝ} (hreal : RealizesInsertionEdge upper old width interpolation j νP νM c d) (horder : theta νM c d ≤ theta νP c d) (hwP : 0 < w νP c d) : interpolation (j + 1) ≤ interpolation j ∧ 0 < width j

The order and denominator conclusions of the local transfer result pass verbatim to adjacent entries of the insertion sequences.

theorem Feige.Lemma43.insertion_conclusions_of_complete {upper old width interpolation : ℕ → ℝ} {j : ℕ} {f : ℝ → ENNReal} {a b c d : ℝ} (hreal : RealizesInsertionEdge upper old width interpolation j (TransferStein.zPlusLaw (MeasureTheory.volume.withDensity f) a) (TransferStein.zMinusLaw (MeasureTheory.volume.withDensity f) b) c d) (hcomplete : CompleteConclusion f a b c d) : insertionTransfer upper old interpolation (c / (c + d)) j = (a - c) / (c + d) * width j * (interpolation j - interpolation (j + 1)) ∧ interpolation (j + 1) ≤ interpolation j ∧ 0 < width j

A full CompleteConclusion immediately supplies every analytic fact needed by the insertion algorithm on a realized edge.

theorem Feige.Lemma43.finiteSignedExp_insertion_conclusions (Fs : List LikelihoodRatio.SignedExpFactor) {upper old width interpolation : ℕ → ℝ} {j : ℕ} {a b c d : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) (hreal : RealizesInsertionEdge upper old width interpolation j (TransferStein.zPlusLaw (MeasureTheory.volume.withDensity (LikelihoodRatio.finiteSignedExpSumDensity Fs)) a) (TransferStein.zMinusLaw (MeasureTheory.volume.withDensity (LikelihoodRatio.finiteSignedExpSumDensity Fs)) b) c d) : insertionTransfer upper old interpolation (c / (c + d)) j = (a - c) / (c + d) * width j * (interpolation j - interpolation (j + 1)) ∧ interpolation (j + 1) ≤ interpolation j ∧ 0 < width j

The local transfer result for finite signed-exponential common parts, now exposed directly in the insertion-sequence interface.

theorem Feige.Lemma43.terminal_insertion_conclusions (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (hpos : μ (Set.Ioi 0) = 0) {upper old width interpolation : ℕ → ℝ} {j : ℕ} {c d : ℝ} (hc : 0 < c) (hd : 0 < d) (hreal : RealizesInsertionEdge upper old width interpolation j (TransferStein.zPlusLaw μ 1) (TransferStein.zMinusLaw μ 1) c d) : insertionTransfer upper old interpolation (c / (c + d)) j = (1 - c) / (c + d) * width j * (interpolation j - interpolation (j + 1)) ∧ interpolation (j + 1) ≤ interpolation j ∧ 0 < width j

The terminal edge changes the distinguished exponential from +E₀ to -E₀. The factorized transfer identity still holds for its arbitrary common law; support on the nonpositive half-line makes the negative endpoint's interpolation parameter zero, which is all the order information needed there.