Documentation

LeanPool.SingleCopyStabilizer.PhysicalExactLearning

The actual amplitude experiment realizes the verified label process. Zero-probability observations are handled without consulting the unknown stabilizer labels in the physical algorithm.

source
theorem LeanPool.SingleCopyStabilizer.PhysicalExactLearning.label_next_of_supported {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) (hu : o.1 ∈ xProjection S.labels) :
PhysicalSampling.labels (QuantumRound.quantumRound S o) = ExactLearning.next (PhysicalSampling.labels S) o

On every possible observation, the physical and algebraic updates agree.

source
def LeanPool.SingleCopyStabilizer.PhysicalExactLearning.failureProbability {ι : Type u_1} [Fintype ι] [DecidableEq ι] :
ℕ → PureStabilizerState ι → ℝ

Failure to reach full diagonal rank, evaluated on the actual Born branching experiment with concrete CNOT and H/HS amplitude updates.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem LeanPool.SingleCopyStabilizer.PhysicalExactLearning.failureProbability_eq_labelProcess {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : ℕ) (S : PureStabilizerState ι) :
    failureProbability t S = ExactLearning.process.failureProbability t (PhysicalSampling.labels S)

    The finite tree probabilities coincide, with all sampling and physical gate hypotheses discharged.

    source
    theorem LeanPool.SingleCopyStabilizer.PhysicalExactLearning.failureProbability_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : ℕ) (S : PureStabilizerState ι) :
    0 ≤ failureProbability t S
    source
    theorem LeanPool.SingleCopyStabilizer.PhysicalExactLearning.failureProbability_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : ℕ) (S : PureStabilizerState ι) :
    failureProbability t S ≤ 1
    source
    theorem LeanPool.SingleCopyStabilizer.PhysicalExactLearning.compression_failure_probability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) :
    failureProbability (SharpExactLearning.roundBudget (Fintype.card ι) δ) S ≤ δ

    Physical adaptive compression with a leading 2n round budget.

    source
    theorem LeanPool.SingleCopyStabilizer.PhysicalExactLearning.compression_failure_probability_after_budget {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) (T : ℕ) (hT : SharpExactLearning.roundBudget (Fintype.card ι) δ ≤ T) :
    failureProbability T S ≤ δ