Documentation

LeanPool.SingleCopyStabilizer.PhysicalSampling

The exact round's actual two-copy Born measurements and independent correction bit induce precisely the finite kernel used in the tail proof.

source
def LeanPool.SingleCopyStabilizer.PhysicalSampling.labels {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) :
ExactLearning.State ι

The Lagrangian label state underlying a physical stabilizer state.

Equations
Instances For
    source
    noncomputable def LeanPool.SingleCopyStabilizer.PhysicalSampling.outcomePMF {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) :
    PMF (ExactLearning.Outcome ι)

    Two independent fresh computational outcomes, their difference, then an independent fair correction bit.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LeanPool.SingleCopyStabilizer.PhysicalSampling.correction_map_apply {ι : Type u_1} [Fintype ι] (u : Measurement.Bits ι) (o : ExactLearning.Outcome ι) :
      (PMF.map (fun (b : ZMod 2) => (u, b)) (FiniteProbability.uniformPMF (ZMod 2))) o = if u = o.1 then 1 / 2 else 0
      source
      theorem LeanPool.SingleCopyStabilizer.PhysicalSampling.outcomePMF_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) :
      (outcomePMF S) o = (bornDifferencePMF S.amplitude ⋯) o.1 / 2
      source
      theorem LeanPool.SingleCopyStabilizer.PhysicalSampling.outcomePMF_eq_kernel {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) :
      (outcomePMF S) o = ENNReal.ofReal (ExactLearning.weight (labels S) o)

      The label process's kernel is derived from the physical sampling PMF.

      source
      theorem LeanPool.SingleCopyStabilizer.PhysicalSampling.outcomePMF_toReal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) :
      ((outcomePMF S) o).toReal = ExactLearning.weight (labels S) o
      source
      theorem LeanPool.SingleCopyStabilizer.PhysicalSampling.outcomePMF_zero_of_not_mem {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) (hu : o.1 ∉ xProjection S.labels) :
      (outcomePMF S) o = 0