Expectations on inserted maximal chains

This file rewrites the chain expectation in terms of the direct inserted states. Together with InsertionK and InsertionAlgebra, it is the bridge from concrete Boolean chains to the pairwise mass-transport calculation in the proof of Theorem 2.1.

theorem Feige.booleanChainExpectation_eq_levelSum {m : ℕ} (γ β : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) (hγ : ∀ (i : Fin m), 0 ≤ γ i) (hβ : ∀ (i : Fin m), 0 ≤ β i) (g : Finset (Fin m) → ℝ) : booleanChainExpectation γ β σ hγ hβ g = ∑ r : Fin (m + 1), chainMass (booleanChainK γ β σ) ↑r * g (chainState σ r)

Expand a Boolean-chain expectation as its finite level sum.

theorem Feige.booleanChainExpectation_insertChainPerm_eq_levelSum {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) (hγ : ∀ (i : Fin (n + 1)), 0 ≤ γ i) (hβ : ∀ (i : Fin (n + 1)), 0 ≤ β i) (g : Finset (Fin (n + 1)) → ℝ) : booleanChainExpectation γ β (insertChainPerm σ J) hγ hβ g = ∑ r : Fin (n + 2), chainMass (booleanChainK γ β (insertChainPerm σ J)) ↑r * g (insertedChainState σ J r)

For an inserted permutation, the same expectation is carried by the direct states C₀,...,C_J,H_J,...,Hₙ.

noncomputable def Feige.insertionLowerPayoff {n : ℕ} (σ : Equiv.Perm (Fin n)) (g : Finset (Fin (n + 1)) → ℝ) (r : ℕ) : ℝ

Payoff at a lifted lower state Cᵣ, with a harmless zero extension.

Equations

• Feige.insertionLowerPayoff σ g r = if hr : r < n + 1 then g (Feige.liftChainState (Feige.chainState σ ⟨r, hr⟩)) else 0

noncomputable def Feige.insertionUpperPayoff {n : ℕ} (σ : Equiv.Perm (Fin n)) (g : Finset (Fin (n + 1)) → ℝ) (r : ℕ) : ℝ

Payoff at a lifted upper state Hᵣ, with a harmless zero extension.

Equations

• Feige.insertionUpperPayoff σ g r = if hr : r < n + 1 then g (insert (Fin.last n) (Feige.liftChainState (Feige.chainState σ ⟨r, hr⟩))) else 0

noncomputable def Feige.revealedLastPayoff {n : ℕ} (p : ℝ) (g : Finset (Fin (n + 1)) → ℝ) (S : Finset (Fin n)) : ℝ

Payoff after independently revealing the new last coordinate with probability p.

Equations

• Feige.revealedLastPayoff p g S = (1 - p) * g (Feige.liftChainState S) + p * g (insert (Fin.last n) (Feige.liftChainState S))

theorem Feige.booleanChainExpectation_revealedLast_eq_pairSum {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (hγ : ∀ (i : Fin (n + 1)), 0 ≤ γ i) (hβ : ∀ (i : Fin (n + 1)), 0 ≤ β i) (p : ℝ) (g : Finset (Fin (n + 1)) → ℝ) : booleanChainExpectation (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) σ ⋯ ⋯ (revealedLastPayoff p g) = ∑ j ∈ Finset.range (n + 1), (independentLowerMass (insertionOldK γ β σ) p j * insertionLowerPayoff σ g j + independentUpperMass (insertionOldK γ β σ) p j * insertionUpperPayoff σ g j)

In expectation form, the old chain followed by an independent Bernoulli reveal expands into the independent lower and upper pair masses.

theorem Feige.insertionLowerPayoff_le_upperPayoff {n : ℕ} (σ : Equiv.Perm (Fin n)) {g : Finset (Fin (n + 1)) → ℝ} (hg : Monotone g) (r : ℕ) : insertionLowerPayoff σ g r ≤ insertionUpperPayoff σ g r

An increasing Boolean-lattice payoff is increasing on every insertion pair Cᵣ ⊆ Hᵣ.

theorem Feige.insertionLevelScore_eq_booleanChainTerm {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) (g : Finset (Fin (n + 1)) → ℝ) (r : Fin (n + 2)) : insertionLevelScore (insertionUpperK γ β σ) (insertionLowerK γ β σ) (fun (q : ℕ) => insertionLowerK γ β σ q - insertionUpperK γ β σ q) (insertionLowerPayoff σ g) (insertionUpperPayoff σ g) ↑J ↑r = chainMass (booleanChainK γ β (insertChainPerm σ J)) ↑r * g (insertedChainState σ J r)

Each level term in the abstract insertion score is the corresponding term of the concrete inserted Boolean-chain expectation.

theorem Feige.insertionPairScore_eq_booleanChainExpectation {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) (hγ : ∀ (i : Fin (n + 1)), 0 ≤ γ i) (hβ : ∀ (i : Fin (n + 1)), 0 ≤ β i) (g : Finset (Fin (n + 1)) → ℝ) : insertionPairScore (insertionUpperK γ β σ) (insertionLowerK γ β σ) (fun (q : ℕ) => insertionLowerK γ β σ q - insertionUpperK γ β σ q) (insertionLowerPayoff σ g) (insertionUpperPayoff σ g) (n + 1) ↑J = booleanChainExpectation γ β (insertChainPerm σ J) hγ hβ g

The canonical pairwise score is exactly the concrete expectation of the corresponding inserted maximal chain.

theorem Feige.exists_insertChainPerm_expectation_ge_of_transfer {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (hγ : ∀ (i : Fin (n + 1)), 0 ≤ γ i) (hβ : ∀ (i : Fin (n + 1)), 0 ≤ β i) {g : Finset (Fin (n + 1)) → ℝ} (hg : Monotone g) (F θ a : ℕ → ℝ) (p c d old : ℝ) (hF : ∀ (r : ℕ), F r = insertionUpperK γ β σ r + θ r * (insertionLowerK γ β σ r - insertionUpperK γ β σ r)) (hθ : Antitone θ) (hθ0 : θ 0 = 1) (hθlast : θ (n + 1) = 0) (hac : ∀ j < n + 1, c ≤ a j) (hcd : 0 < c + d) (hw : ∀ j < n + 1, 0 ≤ insertionLowerK γ β σ j - insertionUpperK γ β σ j) (htransfer : ∀ j < n + 1, insertionTransfer (insertionUpperK γ β σ) F θ p j = (a j - c) / (c + d) * (insertionLowerK γ β σ j - insertionUpperK γ β σ j) * (θ j - θ (j + 1))) (hold : old = ∑ j ∈ Finset.range (n + 1), (independentLowerMass F p j * insertionLowerPayoff σ g j + independentUpperMass F p j * insertionUpperPayoff σ g j)) : ∃ (J : Fin (n + 1)), old ≤ booleanChainExpectation γ β (insertChainPerm σ J) hγ hβ g

Concrete finite conclusion of the chain-insertion step.

All combinatorial and averaging steps have been discharged: the remaining hypotheses are exactly the analytic sequence identities and signs supplied by the exponential-transfer argument.

theorem Feige.exists_insertChainPerm_expectation_ge {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (hγ : ∀ (i : Fin (n + 1)), 0 ≤ γ i) (hβ : ∀ (i : Fin (n + 1)), 0 ≤ β i) {g : Finset (Fin (n + 1)) → ℝ} (hg : Monotone g) (a : ℕ → ℝ) (p c d old : ℝ) (hwidth : ∀ r < n + 1, 0 < insertionWidth γ β σ r) (hθ : Antitone (insertionTheta γ β σ)) (hac : ∀ j < n + 1, c ≤ a j) (hcd : 0 < c + d) (htransfer : ∀ j < n + 1, insertionTransfer (insertionUpperK γ β σ) (insertionOldK γ β σ) (insertionTheta γ β σ) p j = (a j - c) / (c + d) * insertionWidth γ β σ j * (insertionTheta γ β σ j - insertionTheta γ β σ (j + 1))) (hold : old = ∑ j ∈ Finset.range (n + 1), (independentLowerMass (insertionOldK γ β σ) p j * insertionLowerPayoff σ g j + independentUpperMass (insertionOldK γ β σ) p j * insertionUpperPayoff σ g j)) : ∃ (J : Fin (n + 1)), old ≤ booleanChainExpectation γ β (insertChainPerm σ J) hγ hβ g

The chain-insertion conclusion specialized to the actual F,A,B,w,θ sequences of an old Boolean chain. Only strict band positivity, monotonicity of θ, the edgewise transfer identity, and the old-expectation expansion remain as analytic inputs.

theorem Feige.exists_insertChainPerm_dominates_reveal {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (hγ : ∀ (i : Fin (n + 1)), 0 ≤ γ i) (hβ : ∀ (i : Fin (n + 1)), 0 ≤ β i) {g : Finset (Fin (n + 1)) → ℝ} (hg : Monotone g) (a : ℕ → ℝ) (p c d : ℝ) (hwidth : ∀ r < n + 1, 0 < insertionWidth γ β σ r) (hθ : Antitone (insertionTheta γ β σ)) (hac : ∀ j < n + 1, c ≤ a j) (hcd : 0 < c + d) (htransfer : ∀ j < n + 1, insertionTransfer (insertionUpperK γ β σ) (insertionOldK γ β σ) (insertionTheta γ β σ) p j = (a j - c) / (c + d) * insertionWidth γ β σ j * (insertionTheta γ β σ j - insertionTheta γ β σ (j + 1))) : ∃ (J : Fin (n + 1)), booleanChainExpectation (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) σ ⋯ ⋯ (revealedLastPayoff p g) ≤ booleanChainExpectation γ β (insertChainPerm σ J) hγ hβ g

In chain-expectation form, independently revealing the new coordinate is dominated by one concrete insertion of that coordinate into the old maximal chain.