(A.2) for the head's component $j = 0$

Proved

IncentivesInTeams.Conglomerate.appendix_A2_center

by mikedeng1 · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

conditional-expectationindependencep2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1team-theory

Consider a conglomerate model whose component weights are probability weights, a joint strategy $\beta^*$ , a subunit $i$ and a strategy $\beta_i \in B_i$ . Let $\hat y_0$ denote the head's information when $\beta^*/\beta_i$ is played. Then

E\big[v_0[\delta_0^*(\hat y_0(s)), s_0]\big] = E\big[h_0(\hat y_0(s))\big],

where $h_0(y_0)$ is the head's own factor of his conditional expectation under $\beta^*$ (model file): the average of $v_0[\delta_0^*(y_0), t]$ over the head's states $t$ with $\zeta_0^*(t) = z_0$ , for $y_0 = (z_0, m)$ .

This is (A.2) for the component $j = 0$ , which the paper covers by "[the proof for $j = 0$ is strictly analogous]". It is needed because the sum $\sum_{j\ne i}$ in (3.3) runs over $I = \{0, \dots, n\}$ and so includes the head's payoff component.

Preamble

import Mathlib
import Definitions.Def_IncentivesInTeams_Conglomerate_Model

Formal statement

namespace IncentivesInTeams.Conglomerate

theorem appendix_A2_center {ι : Type*} [Fintype ι] [DecidableEq ι] {S₀ : Type*} [Fintype S₀] {S : ι → Type*}
    [∀ i, Fintype (S i)] {Z₀ : Type*} {Z M₀ M : ι → Type*} {D₀ : Type*} {D : ι → Type*}
    (T : Model S₀ S Z₀ Z M₀ M D₀ D) (hT : T.WeightsOK)
    (βs : JointStrategy S₀ S Z₀ Z M₀ M D₀ D) (i : ι)
    (b : SubStrategy (S i) (Z i) (M₀ i) (M i) (D i)) (hb : b ∈ T.B i) :
    T.expect (T.headPayoff (βs.update i b)) =
      T.expect (fun s => T.headFactor βs ((βs.update i b).headInfo s)) := by sorry

end IncentivesInTeams.Conglomerate

Source

Groves, Incentives in Teams, Econometrica 41(4), 1973, p. 630, Appendix, display (A.2) and "[the proof for j = 0 is strictly analogous]"

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. $\iota$ is a finite set of subunits. $S_0$ and each $S_k$ are finite. The weights $P_0$ and $P_k$ are assumed to be probability weights, with $P(s)=P_0(s_0)\prod_kP_k(s_k)$ and $\mathbb E[X]=\sum_sP(s)X(s)$ . The head's payoff is $v_0:D_0\times S_0\to\mathbb R$ .

A joint strategy $\beta$ has head functions $\zeta_0:S_0\to Z_0$ , $\gamma_0^k:Z_0\to M_{0k}$ and $\delta_0:Z_0\times\prod_kM_k\to D_0$ , and subunit functions $\zeta_k$ and $\gamma_k$ . The head's information is

y_0^\beta(s)=\Big(\zeta_0(s_0),\big(\gamma_k(\zeta_k(s_k),\gamma_0^k(\zeta_0(s_0)))\big)_k\Big),

and the head's payoff under $\beta$ is $u_0^\beta(s)=v_0(\delta_0(y_0^\beta(s)),s_0)$ .

For fixed $\beta^*$ and $\bar y=(z_0,m)$ :

H(\bar y)=\operatorname{cavg}_{P_0}\big(\{t\in S_0:\zeta^*_0(t)=z_0\},\ t\mapsto v_0(\delta^*_0(\bar y),t)\big).

Here $\operatorname{cavg}_w(E,X)=\sum_EwX/\sum_Ew$ , with value $0$ when the denominator is $0$ .

Theorem. Take a joint strategy $\beta^*$ , a subunit $i$ , and a subunit- $i$ strategy $b\in B_i$ . Let $\beta^*/b$ be $\beta^*$ with subunit $i$ 's strategy replaced by $b$ . Then

\mathbb E\big[u_0^{\beta^*/b}\big]=\mathbb E\Big[s\mapsto H\big(y_0^{\beta^*/b}(s)\big)\Big].

$\beta^*$ is not required to lie in any strategy set, and no positivity assumption is made.

Degenerate cases. The weight hypothesis forces all state sets to be nonempty. If $\{t:\zeta^*_0(t)=z_0\}$ has $P_0$ -weight $0$ , then $H$ is $0$ there. The existence of $i$ forces $\iota$ to be nonempty.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

(A.2) for the head's component j=0j = 0j=0

(A.2) for the head's component $j = 0$