Algebraic bookkeeping for chain insertion

This file isolates the finite mass calculations in the chain-insertion proof of Theorem 2.1. The analytic content of the exponential transfer step is kept separate: once that step supplies the sign of η, the results below identify the new chain mixture as an upward transfer inside each pair {Cⱼ, Hⱼ}.

def Feige.insertionWeight (θ : ℕ → ℝ) (j : ℕ) : ℝ

The insertion-position weight.

Equations

• Feige.insertionWeight θ j = Feige.chainMass θ j

def Feige.insertedLowerMass (B w θ : ℕ → ℝ) (j : ℕ) : ℝ

Averaged mass placed at the lower state Cⱼ.

Equations

• Feige.insertedLowerMass B w θ j = θ (j + 1) * (B j - B (j + 1)) + Feige.insertionWeight θ j * w j

def Feige.insertedUpperMass (A θ : ℕ → ℝ) (j : ℕ) : ℝ

Averaged mass placed at the upper state Hⱼ.

Equations

• Feige.insertedUpperMass A θ j = (1 - θ (j + 1)) * (A j - A (j + 1))

def Feige.independentLowerMass (F : ℕ → ℝ) (p : ℝ) (j : ℕ) : ℝ

Mass at Cⱼ before replacing the independent Bernoulli reveal.

Equations

• Feige.independentLowerMass F p j = (1 - p) * (F j - F (j + 1))

def Feige.independentUpperMass (F : ℕ → ℝ) (p : ℝ) (j : ℕ) : ℝ

Mass at Hⱼ before replacing the independent Bernoulli reveal.

Equations

• Feige.independentUpperMass F p j = p * (F j - F (j + 1))

def Feige.lowerMassForInsertion (B w : ℕ → ℝ) (J j : ℕ) : ℝ

Mass assigned to Cⱼ by the chain whose insertion rank is J. The state is absent for J < j, has the bridge mass wⱼ for J = j, and has the ordinary B-chain mass for j < J.

Equations

• Feige.lowerMassForInsertion B w J j = if J = j then w j else if j < J then B j - B (j + 1) else 0

def Feige.upperMassForInsertion (A : ℕ → ℝ) (J j : ℕ) : ℝ

Mass assigned to Hⱼ by the chain whose insertion rank is J. This state occurs exactly for J ≤ j.

Equations

• Feige.upperMassForInsertion A J j = if J ≤ j then A j - A (j + 1) else 0

noncomputable def Feige.insertionPairScore (A B w gLower gUpper : ℕ → ℝ) (k J : ℕ) : ℝ

Pairwise expansion of the expectation for the chain whose insertion rank is J.

Equations

• Feige.insertionPairScore A B w gLower gUpper k J = ∑ j ∈ Finset.range k, (Feige.lowerMassForInsertion B w J j * gLower j + Feige.upperMassForInsertion A J j * gUpper j)

noncomputable def Feige.insertionLevelScore (A B w gLower gUpper : ℕ → ℝ) (J r : ℕ) : ℝ

The same inserted-chain score indexed by its consecutive chain level: levels through J are lower states and later levels are upper states.

Equations

• Feige.insertionLevelScore A B w gLower gUpper J r = if r ≤ J then Feige.lowerMassForInsertion B w J r * gLower r else Feige.upperMassForInsertion A J (r - 1) * gUpper (r - 1)

theorem Feige.insertionPairScore_eq_levelScore {A B w gLower gUpper : ℕ → ℝ} {k J : ℕ} (hJk : J < k) : insertionPairScore A B w gLower gUpper k J = ∑ r ∈ Finset.range (k + 1), insertionLevelScore A B w gLower gUpper J r

The pairwise and consecutive-level expansions of one inserted-chain expectation agree.

def Feige.insertionStatisticSequence (A B : ℕ → ℝ) (J r : ℕ) : ℝ

Statistic sequence along the chain with insertion rank J: the pre-insertion levels use B, and the post-insertion levels use A with their index shifted by one.

Equations

• Feige.insertionStatisticSequence A B J r = if r ≤ J then B r else A (r - 1)

theorem Feige.chainMass_insertionStatisticSequence_lower {A B w : ℕ → ℝ} {J j : ℕ} (hjJ : j ≤ J) (hbridge : B j - A j = w j) : chainMass (insertionStatisticSequence A B J) j = lowerMassForInsertion B w J j

At a lower state Cⱼ which is present in the rank-J chain, the adjacent-difference chain mass is exactly the corresponding lower contribution.

theorem Feige.chainMass_insertionStatisticSequence_upper {A B : ℕ → ℝ} {J j : ℕ} (hJj : J ≤ j) : chainMass (insertionStatisticSequence A B J) (j + 1) = upperMassForInsertion A J j

At an upper state Hⱼ, present exactly for J ≤ j, the adjacent-difference chain mass is its upper contribution.

def Feige.insertionTransfer (A F θ : ℕ → ℝ) (p : ℝ) (j : ℕ) : ℝ

The upward mass-transfer coefficient.

Equations

• Feige.insertionTransfer A F θ p j = Feige.insertedUpperMass A θ j - Feige.independentUpperMass F p j

theorem Feige.inserted_pair_total {A B F w θ : ℕ → ℝ} (j : ℕ) (hB : ∀ (r : ℕ), B r = A r + w r) (hF : ∀ (r : ℕ), F r = A r + θ r * w r) : insertedLowerMass B w θ j + insertedUpperMass A θ j = F j - F (j + 1)

The lower and upper mass formulas preserve the total mass of each pair {Cⱼ, Hⱼ}.

theorem Feige.independent_pair_total (F : ℕ → ℝ) (p : ℝ) (j : ℕ) : independentLowerMass F p j + independentUpperMass F p j = F j - F (j + 1)

theorem Feige.lower_difference_eq_neg_transfer {A B F w θ : ℕ → ℝ} {p : ℝ} (j : ℕ) (hB : ∀ (r : ℕ), B r = A r + w r) (hF : ∀ (r : ℕ), F r = A r + θ r * w r) : insertedLowerMass B w θ j - independentLowerMass F p j = -insertionTransfer A F θ p j

Equal pair totals force the difference to be a within-pair transfer: the lower state loses exactly the mass gained by the upper state.

theorem Feige.upward_transfer_improves {newLower newUpper oldLower oldUpper η gLower gUpper : ℝ} (hlower : newLower - oldLower = -η) (hupper : newUpper - oldUpper = η) (hη : 0 ≤ η) (hg : gLower ≤ gUpper) : oldLower * gLower + oldUpper * gUpper ≤ newLower * gLower + newUpper * gUpper

A nonnegative transfer improves every increasing payoff on the pair.

theorem Feige.sum_upward_transfers_improve {k : ℕ} {newLower newUpper oldLower oldUpper η gLower gUpper : ℕ → ℝ} (hlower : ∀ j < k, newLower j - oldLower j = -η j) (hupper : ∀ j < k, newUpper j - oldUpper j = η j) (hη : ∀ j < k, 0 ≤ η j) (hg : ∀ j < k, gLower j ≤ gUpper j) : ∑ j ∈ Finset.range k, (oldLower j * gLower j + oldUpper j * gUpper j) ≤ ∑ j ∈ Finset.range k, (newLower j * gLower j + newUpper j * gUpper j)

Summing the pairwise upward transfers proves the expectation comparison.

theorem Feige.insertionWeight_nonneg {θ : ℕ → ℝ} (hθ : Antitone θ) (j : ℕ) : 0 ≤ insertionWeight θ j

The insertion-position weights are nonnegative when θ decreases.

theorem Feige.sum_insertionWeight (θ : ℕ → ℝ) (k : ℕ) : ∑ j ∈ Finset.range k, insertionWeight θ j = θ 0 - θ k

The insertion-position weights telescope from θ 0 to θ k.

theorem Feige.sum_insertionWeight_eq_one {θ : ℕ → ℝ} {k : ℕ} (hzero : θ 0 = 1) (hend : θ k = 0) : ∑ j ∈ Finset.range k, insertionWeight θ j = 1

Under the endpoint conditions θ 0 = 1 and θ k = 0, the insertion weights sum to one.

theorem Feige.sum_lowerMassForInsertion {B w θ : ℕ → ℝ} {j k : ℕ} (hjk : j < k) : ∑ J ∈ Finset.range k, insertionWeight θ J * lowerMassForInsertion B w J j = (∑ J ∈ Finset.Ico (j + 1) k, insertionWeight θ J) * (B j - B (j + 1)) + insertionWeight θ j * w j

Averaging the actual Cⱼ mass over all insertion ranks separates into the single bridge rank and the strictly later ranks.

theorem Feige.sum_upperMassForInsertion {A θ : ℕ → ℝ} {j k : ℕ} (hjk : j < k) : ∑ J ∈ Finset.range k, insertionWeight θ J * upperMassForInsertion A J j = (∑ J ∈ Finset.range (j + 1), insertionWeight θ J) * (A j - A (j + 1))

Averaging the actual Hⱼ mass over all insertion ranks keeps exactly the ranks through j.

theorem Feige.sum_insertionWeight_after {θ : ℕ → ℝ} {j k : ℕ} (hjk : j < k) (hend : θ k = 0) : ∑ J ∈ Finset.Ico (j + 1) k, insertionWeight θ J = θ (j + 1)

The total insertion weight strictly after rank j. This is the coefficient of Bⱼ - Bⱼ₊₁ in the averaged mass at Cⱼ.

theorem Feige.sum_insertionWeight_through {θ : ℕ → ℝ} (j : ℕ) (hzero : θ 0 = 1) : ∑ J ∈ Finset.range (j + 1), insertionWeight θ J = 1 - θ (j + 1)

The total insertion weight through rank j. This is the coefficient of Aⱼ - Aⱼ₊₁ in the averaged mass at Hⱼ.

theorem Feige.averaged_lower_mass_eq_insertedLowerMass {B w θ : ℕ → ℝ} {j k : ℕ} (hjk : j < k) (hend : θ k = 0) : (∑ J ∈ Finset.Ico (j + 1) k, insertionWeight θ J) * (B j - B (j + 1)) + insertionWeight θ j * w j = insertedLowerMass B w θ j

The averaged lower-mass formula obtained by separating the insertion rank J = j from all later ranks.

theorem Feige.averaged_upper_mass_eq_insertedUpperMass {A θ : ℕ → ℝ} (j : ℕ) (hzero : θ 0 = 1) : (∑ J ∈ Finset.range (j + 1), insertionWeight θ J) * (A j - A (j + 1)) = insertedUpperMass A θ j

The averaged upper-mass formula obtained by summing over all insertion ranks J ≤ j.

theorem Feige.weighted_lowerMassForInsertion_eq {B w θ : ℕ → ℝ} {j k : ℕ} (hjk : j < k) (hend : θ k = 0) : ∑ J ∈ Finset.range k, insertionWeight θ J * lowerMassForInsertion B w J j = insertedLowerMass B w θ j

The full weighted rank average gives the lower-mass formula.

theorem Feige.weighted_upperMassForInsertion_eq {A θ : ℕ → ℝ} {j k : ℕ} (hjk : j < k) (hzero : θ 0 = 1) : ∑ J ∈ Finset.range k, insertionWeight θ J * upperMassForInsertion A J j = insertedUpperMass A θ j

The full weighted rank average gives the upper-mass formula.

theorem Feige.weighted_insertionPairScore_eq {A B w θ gLower gUpper : ℕ → ℝ} {k : ℕ} (hθ0 : θ 0 = 1) (hθk : θ k = 0) : ∑ J ∈ Finset.range k, insertionWeight θ J * insertionPairScore A B w gLower gUpper k J = ∑ j ∈ Finset.range k, (insertedLowerMass B w θ j * gLower j + insertedUpperMass A θ j * gUpper j)

Averaging the complete pairwise scores over insertion ranks gives the averaged lower and upper masses.

theorem Feige.exists_score_ge_of_le_convex_average {k : ℕ} (hk : 0 < k) {weight score : ℕ → ℝ} {old : ℝ} (hweight : ∀ j < k, 0 ≤ weight j) (hsum : ∑ j ∈ Finset.range k, weight j = 1) (hold : old ≤ ∑ j ∈ Finset.range k, weight j * score j) : ∃ j < k, old ≤ score j

A convex average cannot exceed all of its entries. This is the final finite step selecting one insertion position from the averaged chain comparison.

theorem Feige.insertionTransfer_nonneg_of_identity {η a c d w thetaPlus thetaMinus : ℝ} (hid : η = (a - c) / (c + d) * w * (thetaPlus - thetaMinus)) (hac : c ≤ a) (hcd : 0 < c + d) (hw : 0 ≤ w) (hθ : thetaMinus ≤ thetaPlus) : 0 ≤ η

The local transfer identity identifies the insertion coefficient η; positivity of its four factors gives the upward transfer direction.

theorem Feige.localInsertion_average_pair_payoff_le {k : ℕ} {A B F w θ a : ℕ → ℝ} {p c d : ℝ} {gLower gUpper : ℕ → ℝ} (hB : ∀ (r : ℕ), B r = A r + w r) (hF : ∀ (r : ℕ), F r = A r + θ r * w r) (hθ : Antitone θ) (hac : ∀ j < k, c ≤ a j) (hcd : 0 < c + d) (hw : ∀ j < k, 0 ≤ w j) (htransfer : ∀ j < k, insertionTransfer A F θ p j = (a j - c) / (c + d) * w j * (θ j - θ (j + 1))) (hg : ∀ j < k, gLower j ≤ gUpper j) : ∑ j ∈ Finset.range k, (independentLowerMass F p j * gLower j + independentUpperMass F p j * gUpper j) ≤ ∑ j ∈ Finset.range k, (insertedLowerMass B w θ j * gLower j + insertedUpperMass A θ j * gUpper j)

The finite mass-transport conclusion of the chain-insertion step.

Once the exponential transfer identity has supplied the required factorized transfer on every edge, the independently revealed coordinate is dominated by the averaged inserted-chain law for every payoff which is increasing on each pair Cⱼ ⊆ Hⱼ. All remaining hypotheses are the corresponding analytic and probabilistic identities.

theorem Feige.exists_localInsertion_score_of_transfer {k : ℕ} (hk : 0 < k) {A B F w θ a : ℕ → ℝ} {p c d old : ℝ} {gLower gUpper score : ℕ → ℝ} (hB : ∀ (r : ℕ), B r = A r + w r) (hF : ∀ (r : ℕ), F r = A r + θ r * w r) (hθ : Antitone θ) (hθ0 : θ 0 = 1) (hθk : θ k = 0) (hac : ∀ j < k, c ≤ a j) (hcd : 0 < c + d) (hw : ∀ j < k, 0 ≤ w j) (htransfer : ∀ j < k, insertionTransfer A F θ p j = (a j - c) / (c + d) * w j * (θ j - θ (j + 1))) (hg : ∀ j < k, gLower j ≤ gUpper j) (hold : old = ∑ j ∈ Finset.range k, (independentLowerMass F p j * gLower j + independentUpperMass F p j * gUpper j)) (haverage : ∑ j ∈ Finset.range k, insertionWeight θ j * score j = ∑ j ∈ Finset.range k, (insertedLowerMass B w θ j * gLower j + insertedUpperMass A θ j * gUpper j)) : ∃ j < k, old ≤ score j

Full finite selection step in the chain-insertion argument.

The two equalities hold and haverage are precisely the expansions of the old hybrid expectation and of the convex average of inserted-chain expectations. The theorem first applies the upward-transport comparison and then selects one insertion rank from that convex average.

theorem Feige.exists_insertionPairScore_of_transfer {k : ℕ} (hk : 0 < k) {A B F w θ a : ℕ → ℝ} {p c d old : ℝ} {gLower gUpper : ℕ → ℝ} (hB : ∀ (r : ℕ), B r = A r + w r) (hF : ∀ (r : ℕ), F r = A r + θ r * w r) (hθ : Antitone θ) (hθ0 : θ 0 = 1) (hθk : θ k = 0) (hac : ∀ j < k, c ≤ a j) (hcd : 0 < c + d) (hw : ∀ j < k, 0 ≤ w j) (htransfer : ∀ j < k, insertionTransfer A F θ p j = (a j - c) / (c + d) * w j * (θ j - θ (j + 1))) (hg : ∀ j < k, gLower j ≤ gUpper j) (hold : old = ∑ j ∈ Finset.range k, (independentLowerMass F p j * gLower j + independentUpperMass F p j * gUpper j)) : ∃ j < k, old ≤ insertionPairScore A B w gLower gUpper k j

The finite chain-insertion conclusion with the inserted-chain score expanded canonically into its Cⱼ/Hⱼ pairs. Unlike exists_localInsertion_score_of_transfer, this theorem no longer asks for the averaged-score identity as an external hypothesis.