Provedattentionresidual-seriesexternal-review-4

Tile factorization into marginal and conditional cost factors

For all $\htmlData{mx=1}{T, J \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=5}{\pi, r : \htmlData{mx=0}{T} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{J} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{R}}}$ and $\htmlData{mx=3}{P, R : \htmlData{mx=0}{T} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , if $\htmlData{mx=4}{\forall t,\ \htmlData{mx=2}{\htmlData{mx=0}{P}(\htmlData{mx=1}{t})} \mathrel{\htmlData{mx=3}{\neq}} 0}$ , $\htmlData{mx=4}{\forall t,\ \htmlData{mx=2}{\htmlData{mx=0}{R}(\htmlData{mx=1}{t})} \mathrel{\htmlData{mx=3}{\neq}} 0}$ and $\htmlData{mx=5}{\forall t, j,\ \htmlData{mx=3}{\htmlData{mx=0}{r}(\htmlData{mx=1}{t}, \htmlData{mx=2}{j})} \mathrel{\htmlData{mx=4}{\neq}} 0}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{T}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}}$ ), then

\begin{aligned} & \left(\htmlData{mx=29}{\sum_{t} \htmlData{mx=28}{\htmlData{mx=8}{\frac{\htmlData{mx=4}{\htmlData{mx=3}{\htmlData{mx=1}{P}(\htmlData{mx=2}{t})}^{2}}}{\htmlData{mx=7}{\htmlData{mx=5}{R}(\htmlData{mx=6}{t})}}} \cdot \left(\htmlData{mx=27}{\sum_{j} \htmlData{mx=26}{\frac{\htmlData{mx=17}{\left(\htmlData{mx=16}{\frac{\htmlData{mx=12}{\htmlData{mx=9}{\pi}(\htmlData{mx=10}{t}, \htmlData{mx=11}{j})}}{\htmlData{mx=15}{\htmlData{mx=13}{P}(\htmlData{mx=14}{t})}}}\right)^{2}}}{\htmlData{mx=25}{\frac{\htmlData{mx=21}{\htmlData{mx=18}{r}(\htmlData{mx=19}{t}, \htmlData{mx=20}{j})}}{\htmlData{mx=24}{\htmlData{mx=22}{R}(\htmlData{mx=23}{t})}}}}}}\right)}}\right) \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=41}{\sum_{t} \htmlData{mx=40}{\sum_{j} \htmlData{mx=39}{\frac{\htmlData{mx=34}{\htmlData{mx=33}{\htmlData{mx=30}{\pi}(\htmlData{mx=31}{t}, \htmlData{mx=32}{j})}^{2}}}{\htmlData{mx=38}{\htmlData{mx=35}{r}(\htmlData{mx=36}{t}, \htmlData{mx=37}{j})}}}}} \end{aligned}

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
x ∈ TVariables: T, J range over Type: the statement must hold for every choice. ((T J : Type))
Fintype: Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application: Fintype applied to T. Lean writes f x; papers write f(x). (Fintype T)
x : TVariables: π, r range over T → J → ℝ: the statement must hold for every choice. ((π r : T → J → ℝ))
∀For all: The statement after the comma holds for every t. (∀ t,P t≠0)
=Equality: ∑ t, P(t)^2/R(t) · (∑ j, (π(t, j)/P(t))^2/(r(t, j)/R(t))) and ∑ t, ∑ j, π(t, j)^2/r(t, j) are the same. ((∑ t,P t^2/R t*(∑ j,(π t j/P t)^2/(r t …)
⟹Implies: If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (J → ℝ)
≠Not equal: P(t) and 0 are different. (P t≠0)
aᵇPower: P(t) raised to the power 2. (P t^2)
a/bDivision: P(t)^2 divided by R(t). In Lean, dividing by 0 gives 0. (P t^2/R t)
·Multiplication: P(t)^2/R(t) times ∑ j, (π(t, j)/P(t))^2/(r(t, j)/R(t)). (P t^2/R t*(∑ j,(π t j/P t)^2/(r t j/R t…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
∑Summation: Add up (π(t, j)/P(t))^2/(r(t, j)/R(t)) for every j. (∑ j,(π t j/P t)^2/(r t j/R t))
πPi: The ratio of a circle's circumference to its diameter, ≈ 3.14159. (π)

theorem tile-conditional-factorization {T J : Type} [Fintype T] [Fintype J] (π r : T → J → ℝ) (P R : T → ℝ) (hP : ∀ t,P t≠0) (hR : ∀ t,R t≠0) (hr : ∀ t j,r t j≠0) :
    (∑ t,P t^2/R t*(∑ j,(π t j/P t)^2/(r t j/R t)))=∑ t,∑ j,π t j^2/r t j

Exact finite rectangular-tile algebra, with nonzero supplied target/proposal tile masses and key proposal entries. When those supplied masses are the actual marginals this is the conditional chi-square decomposition. Arbitrary ragged partitions, efficient sampling and GPU costs are not formalized here.

How it was proved

Proved: 6 October 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 12 lines of Lean

Tile factorization into marginal and conditional cost factors

How it was proved

More proved statements