Conditionally linear functions #

Blueprint def:cl-function (paper linear.tex, Definition def:cl-func; ledger node 1.1.2). The question distribution of every game in the pipeline is conditionally linear: linear maps applied in stages to complementary register subspaces of V = F^ι, the register subspace and the linear map of each stage being allowed to depend on the outputs of the previous stages.

Presentations and functions #

The paper defines the set of ℓ-level CL functions on V inductively: the 0-level one is the zero function, and an ℓ-level one is any L of the form L(x) = L₁(x^{V₁}) + L_{>1, L₁(x^{V₁})}(x^{V_{>1}}) for complementary register subspaces V₁ ⊕ V_{>1} = V, a linear map L₁ on V₁, and (ℓ-1)-level CL functions L_{>1,v} on V_{>1}, one for each value v of L₁. Everything downstream — the structure lemma lem:cl-kth, the query interface of a sampler, the hiding tests of introspection — works with the decomposition data, which the function does not determine. So the Lean object is the data:

MIPRE.CL.CLFun F ι ℓ is the type of ℓ-level presentations on the ambient space ι → F. A presentation of level ℓ + 1 is cons S L₁ next: the coordinates S : Finset ι of the first register subspace V₁ = V_S, the first linear map L₁ : RegLinear F S, and the continuation next : (ι → F) → CLFun F ι ℓ, indexed by the value of L₁.
CLFun.eval is the function presented: eval (cons S L₁ next) x = L₁ x + eval (next (L₁ x)) (x^{V_{Sᶜ}}).
CLFun.SupportedOn P T says that P is a presentation on V_T in the paper's sense: S ⊆ T, and every continuation is on V_{T \ S}. The paper's V_{>1} is V_{T \ S}; it is not stored, because the level-0 presentation zero is "the zero function on V_{T'}" for every T' (exactly as in the paper), and this keeps every construction free of dependent-type transport.
MIPRE.CL.IsCLFun ℓ T f is the paper's notion itself: some ℓ-level presentation on V_T evaluates to f.

Two departures from the letter of the paper, both harmless: continuations are indexed by all vectors rather than by the values of L₁ (the others are never evaluated), and there is one ambient space F^ι throughout, register subspaces of it playing the role of the paper's V_{>1}, U ⊕ V, and so on.

The structure lemma (`lem:cl-kth`) #

lem:cl-kth attaches to an ℓ-level CL function its marginals L_{≤k}, factor spaces V_{k,u} and stage maps L_{k,u}, u being the prefix L_{<k}(x). Here:

CLFun.truncate k P presents the k-th marginal (P.truncate ℓ = P, truncate_self), padded with trivial levels when k exceeds the level (CLFun.lift, the paper's rk:higher-level);
CLFun.factorAt P k x and CLFun.mapAt P k x are the register subspace and the linear map applied at stage k + 1 on the input x. They depend on x only through the prefix L_{≤k}(x): CLFun.factorOfPrefix and CLFun.mapOfPrefix compute them from that prefix alone (SupportedOn.factorOfPrefix_eval, SupportedOn.mapOfPrefix_eval), which is what the factor and linear queries of a sampler answer;
SupportedOn.eval_truncate_eq_sum is the decomposition L_{≤k}(x) = ∑_{i ≤ k} x^{L_i}, and SupportedOn.disjoint_factorAt, SupportedOn.factorAt_subset say that the factor spaces along a run are disjoint register subspaces of V_T. CLFun.ExactlyOn P T is the strengthening under which they partition T (ExactlyOn.biUnion_factorAt) — item (2) of lem:cl-kth, which samplers are required to satisfy.

Conditionally linear functions #

Presentations and functions #

The structure lemma (lem:cl-kth) #

Support #

Levels: padding and marginals #

Exact support #

Evaluation #

Evaluation of padded and truncated presentations #

The data of a stage #

Stage data from the prefix #

The paper's notion #

The structure lemma (`lem:cl-kth`) #