Splitting a finite product law at its last coordinate #
These identities are the finite-sum/Tonelli layer used in the two-point
induction for Theorem 2.1. Every high set on Fin (n + 1) is uniquely a
lifted old high set, with or without the last coordinate.
theorem
Feige.highSetMass_lift
{n : ℕ}
(p : Fin (n + 1) → ℝ)
(S : Finset (Fin n))
:
highSetMass p (liftChainState S) = (1 - p (Fin.last n)) * highSetMass (fun (i : Fin n) => p i.castSucc) S
Product mass of a high set not containing the last coordinate.
theorem
Feige.highSetMass_insert_last
{n : ℕ}
(p : Fin (n + 1) → ℝ)
(S : Finset (Fin n))
:
highSetMass p (insert (Fin.last n) (liftChainState S)) = p (Fin.last n) * highSetMass (fun (i : Fin n) => p i.castSucc) S
Product mass of the corresponding high set containing the last coordinate.
theorem
Feige.sum_powerset_succ
{n : ℕ}
(f : Finset (Fin (n + 1)) → ℝ)
:
∑ S ∈ Finset.univ.powerset, f S = ∑ T ∈ Finset.univ.powerset, (f (liftChainState T) + f (insert (Fin.last n) (liftChainState T)))
Reindexing all subsets of Fin (n + 1) by an old subset and a last
coordinate bit.
theorem
Feige.productHighSetExpectation_succ
{n : ℕ}
(p : Fin (n + 1) → ℝ)
(g : Finset (Fin (n + 1)) → ℝ)
:
productHighSetExpectation p g = productHighSetExpectation (fun (i : Fin n) => p i.castSucc) (revealedLastPayoff (p (Fin.last n)) g)
Product expectation recursion at the last coordinate.