OAI/InformationTheory/AmplitudeDamping/SequentialDecoder.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GAD.finiteProjectors line 13
2. theorem OAI.GAD.finiteProjectors_projection line 17
3. theorem OAI.GAD.finiteProjectors_apply line 25
4. def OAI.GAD.sequentialMeasurement line 28
5. theorem OAI.GAD.sequentialMeasurement_pos line 32
6. theorem OAI.GAD.sequentialMeasurement_sum line 36
7. theorem OAI.GAD.sequentialMeasurement_remainder line 54
8. theorem OAI.GAD.complete_submeasurement line 67
9. theorem OAI.GAD.sequentialMeasurement_success line 91
10. theorem OAI.GAD.sequential_decoder_bound line 103

    Source documentation

    Sequential decoding preceded by a global typical-subspace test.

    theorem sequential_decoder_bound {M : ℕ} (hM : 0 < M) (P : Matrix ι ι ℂ) (hP : IsProjection P)
        (Q A : Fin M → Matrix ι ι ℂ) (hQ : ∀ m, IsProjection (Q m)) (hA : ∀ m, IsState (A m)) :
        ∃ D : Fin M → Matrix ι ι ℂ, (∀ m, (D m).PosSemidef) ∧ (∑ m, D m=1) ∧
          ∀ m, 1-(D m*A m).trace.re ≤
            9*(1-(P*A m).trace.re)+8*(1-(Q m*A m).trace.re)+
              4*∑ j : Fin M, if j=m then 0 else (Q j*(P*A m*P)).trace.re := by
    …

    Mentions: OAI.GAD.IsProjection, OAI.GAD.IsState