Closure properties of conditionally linear functions, and CL distributions #
Paper linear.tex: concatenation (lem:cl-concat) and direct sums (lem:cl-func-prod) of
conditionally linear functions, and the conditionally linear distribution of a pair of CL
functions (def:cl-dist); blueprint def:cl-function and lem:cl-closure, ledger node
1.1.2.
Both constructions are on presentations (MIPRE.CL.CLFun) and are hypothesis-free; the
hypotheses of the paper's lemmas — the pieces live on disjoint register subspaces — enter only
in the evaluation lemmas (SupportedOn.eval_concat, SupportedOn.eval_directSum), which say
that the constructions present the functions the paper writes down, and in the support
lemmas. The paper's statements about functions follow as IsCLFun.concat and
IsCLFun.directSum.
CLFun.concat L R: runL(levelk), then theR_u(levelℓ) selected by its output; levelℓ + k— the paper'sT(x) = L(x^U) + R_{L(x^U)}(x^V)onU ⊕ V, here forLonV_U, theR_uonV_W,UandWdisjoint.CLFun.directSum P Q: stage by stage, the register subspaces are joined and the two continuations run side by side, each selected by its own component of the joint output; the paper's⊕ⱼ L⁽ʲ⁾, two summands at a time (liftNpads to a common level, the paper'sℓ = maxⱼ ℓⱼ).MIPRE.CL.clDist L R: the law of(L x, R x)forxuniform, as a real-valued probability mass function on pairs, the format ofMIPRE.Game.
The paper's third closure property, downsizing to 𝔽₂ (lem:cl-downsize), needs the self-dual
bases of blueprint lem:self-dual-basis and is not here.
Concatenation (lem:cl-concat) #
The concatenation of L (level k) with the family R (level ℓ): run L, then the
R_u selected by its output u. The paper's T(x) = L(x^U) + R_{L(x^U)}(x^V); here U and
V are the supports of the two sides (SupportedOn.eval_concat).
Equations
- MIPRE.CL.CLFun.zero.concat x✝ = x✝ 0
- (MIPRE.CL.CLFun.cons S L₁ next).concat x✝ = MIPRE.CL.CLFun.cons S L₁ fun (v : ι → F) => (next v).concat fun (w : ι → F) => x✝ (v + w)
Instances For
Direct sums (lem:cl-func-prod) #
The direct sum of two presentations of the same level (lem:cl-func-prod, two summands;
liftN pads to a common level): stage by stage, the register subspaces are joined and the
continuations run side by side, each selected by its own component of the joint output.
Equations
- One or more equations did not get rendered due to their size.
- MIPRE.CL.CLFun.zero.directSum MIPRE.CL.CLFun.zero = MIPRE.CL.CLFun.zero
Instances For
Evaluation #
The concatenation presents x ↦ L(x) + R_{L(x)}(x), when L is on V_U, the R_u on
V_W, and U, W are disjoint.
The direct sum presents the sum of the two functions, when they are on disjoint register subspaces.
The paper's statements #
lem:cl-concat: if f is a k-level CL function on V_U and each g u an ℓ-level
one on V_W, U and W disjoint, then x ↦ f x + g (f x) x is a (k + ℓ)-level CL
function on V_{U ∪ W}.
lem:cl-func-prod, two summands of the same level: the sum of an ℓ-level CL function on
V_T and one on V_{T'}, T and T' disjoint, is an ℓ-level CL function on V_{T ∪ T'}.
lem:cl-func-prod with summands of different levels: the sum is CL of level the maximum.
Conditionally linear distributions (def:cl-dist) #
The conditionally linear distribution of a pair of functions (def:cl-dist): the law of
(L x, R x) for x uniform in F^ι, as a real-valued probability mass function on pairs, the
format of the question distribution of a MIPRE.Game.
Equations
- MIPRE.CL.clDist L R a b = ↑{x : ι → F | L x = a ∧ R x = b}.card / ↑(Fintype.card (ι → F))