The actual probability law of a CL prefix

The weight is the pushforward of the uniform computational seed. Its Born and normalized-trace descriptions are proved, rather than supplied as extra premises. Restriction to the actual prefix image is a normalized distribution.

noncomputable def MIPRE.Introspection.readoutWeight {I : Type u_1} {X : Type u_2} [Fintype I] (f : I → X) (x : X) : ℝ

The law of a function of a uniform finite seed.

Equations

• MIPRE.Introspection.readoutWeight f x = MIPRE.SampledGame.dist f (fun (x : I) => ()) x ()

theorem MIPRE.Introspection.readoutWeight_eq_card {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq X] (f : I → X) (x : X) : readoutWeight f x = ↑{i : I | f i = x}.card / ↑(Fintype.card I)

theorem MIPRE.Introspection.readoutWeight_nonneg {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq X] (f : I → X) (x : X) : 0 ≤ readoutWeight f x

theorem MIPRE.Introspection.sum_readoutWeight {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq X] [Nonempty I] (f : I → X) : ∑ x : X, readoutWeight f x = 1

theorem MIPRE.Introspection.readout_const_unit {I : Type u_1} [Fintype I] [DecidableEq I] : readout (fun (x : I) => ()) () = 1

theorem MIPRE.Introspection.stateSqNorm_registerEPR_readout {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq X] (f : I → X) (x : X) : stateSqNorm (registerEPR I) (readout f x) = readoutWeight f x

The squared norm selected by a prefix projector is its actual uniform seed probability.

def MIPRE.Introspection.prefixOutcomes {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) : Finset (ι → F)

The actual possible outputs of the truncated CL sampler.

Equations

• MIPRE.Introspection.prefixOutcomes P k = Finset.image (MIPRE.CL.CLFun.truncate k P).eval Finset.univ

noncomputable def MIPRE.Introspection.prefixWeight {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : ℝ

The paper's prefix distribution, before restricting to its support.

Equations

• MIPRE.Introspection.prefixWeight P k y = MIPRE.Introspection.readoutWeight (MIPRE.CL.CLFun.truncate k P).eval y

theorem MIPRE.Introspection.prefixWeight_eq_card {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : prefixWeight P k y = ↑{z : ι → F | (CL.CLFun.truncate k P).eval z = y}.card / ↑(Fintype.card (ι → F))

theorem MIPRE.Introspection.prefixWeight_nonneg {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : 0 ≤ prefixWeight P k y

theorem MIPRE.Introspection.sum_prefixWeight {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) : ∑ y : ι → F, prefixWeight P k y = 1

theorem MIPRE.Introspection.prefixWeight_pos_iff {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : 0 < prefixWeight P k y ↔ y ∈ prefixOutcomes P k

theorem MIPRE.Introspection.prefixWeight_eq_zero {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) (hy : y ∉ prefixOutcomes P k) : prefixWeight P k y = 0

theorem MIPRE.Introspection.sum_prefixWeight_supported {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) : ∑ y : ↥(prefixOutcomes P k), prefixWeight P k ↑y = 1

Restricting the prefix law to attainable outputs preserves normalization.

theorem MIPRE.Introspection.hidingPrefixOp_weight {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Algebra (ZMod 2) F] (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : stateSqNorm (registerEPR (ι → F)) (Honest.hidingPrefixOp P k (some y)) = prefixWeight P k y

The concrete honest prefix measurement has exactly the actual CL law.