Algebraic part of the exponential transfer identity

This file isolates the purely algebraic end of the local exponential transfer step used in the proof of Theorem 2.1. All probability quantities are represented by real numbers. The two Stein identities, together with

• wε = uε + vε,
• Bε = Aε + wε,
• Fε = Bε - vε, and
• θε = uε / wε,

imply the final factorized transfer identity. No order or probabilistic hypotheses are needed for these implications; only the denominators have to be nonzero.

theorem Feige.exponentialTransfer_eq24 {a b c d uPlus uMinus vPlus vMinus wPlus wMinus APlus AMinus BPlus BMinus : ℝ} (hwPlus : wPlus = uPlus + vPlus) (hwMinus : wMinus = uMinus + vMinus) (hBPlus : BPlus = APlus + wPlus) (hBMinus : BMinus = AMinus + wMinus) (hA : d * (APlus - AMinus) = a * uPlus + b * uMinus) (hB : c * (BPlus - BMinus) = a * vPlus + b * vMinus) : (c + d) * (APlus - AMinus) = (a - c) * wPlus + (b + c) * wMinus

An intermediate identity obtained from the Stein relations after substituting Bε = Aε + wε and wε = uε + vε.

theorem Feige.exponentialTransfer_eq25 {a b c vPlus vMinus BPlus BMinus FPlus FMinus : ℝ} (hFPlus : FPlus = BPlus - vPlus) (hFMinus : FMinus = BMinus - vMinus) (hB : c * (BPlus - BMinus) = a * vPlus + b * vMinus) : c * (FPlus - FMinus) = (a - c) * vPlus + (b + c) * vMinus

A second intermediate identity obtained after substituting Fε = Bε - vε.

theorem Feige.one_sub_theta_mul_w {uPlus vPlus wPlus thetaPlus : ℝ} (hw : wPlus = uPlus + vPlus) (hw0 : wPlus ≠ 0) (htheta : thetaPlus = uPlus / wPlus) : (1 - thetaPlus) * wPlus = vPlus

The definition θ = u / w, rewritten without division.

theorem Feige.exponentialTransfer_identity {a b c d uPlus uMinus vPlus vMinus wPlus wMinus APlus AMinus BPlus BMinus FPlus FMinus thetaPlus thetaMinus : ℝ} (hwPlus : wPlus = uPlus + vPlus) (hwMinus : wMinus = uMinus + vMinus) (hwPlus0 : wPlus ≠ 0) (hwMinus0 : wMinus ≠ 0) (hBPlus : BPlus = APlus + wPlus) (hBMinus : BMinus = AMinus + wMinus) (hFPlus : FPlus = BPlus - vPlus) (hFMinus : FMinus = BMinus - vMinus) (hthetaPlus : thetaPlus = uPlus / wPlus) (hthetaMinus : thetaMinus = uMinus / wMinus) (hA : d * (APlus - AMinus) = a * uPlus + b * uMinus) (hB : c * (BPlus - BMinus) = a * vPlus + b * vMinus) (hcd0 : c + d ≠ 0) : (1 - thetaMinus) * (APlus - AMinus) - c / (c + d) * (FPlus - FMinus) = (a - c) / (c + d) * wPlus * (thetaPlus - thetaMinus)

The purely algebraic derivation of the factorized transfer identity.

The assumptions spell out every definitional relation among the abstract probability quantities. Positivity from the probabilistic statement is stronger than the nonvanishing assumptions used here.