OAI/InformationTheory/AmplitudeDamping/Naimark.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GAD.naimark line 15
  2. theorem OAI.GAD.naimark_isometry line 19
  3. theorem OAI.GAD.naimark_block line 30
  4. theorem OAI.GAD.naimark_success line 40
  5. theorem OAI.GAD.blockProjection_injection line 49
  6. theorem OAI.GAD.exists_orthogonal_factors line 56

    Source documentation

    Approximate orthogonalization of well decoded states in a Naimark dilation.

    theorem exists_orthogonal_factors (A D : μ → Matrix ι ι ℂ)
    (hA : ∀ m, IsState (A m)) (hD : ∀ m, (D m).PosSemidef) (hDs : ∑ m, D m=1) :
    ∃ Y : μ → Matrix (ι × μ) ι ℂ,
      (∀ m, mass (Y m)=1) ∧ (∀ m, blockProjection (ι := ι) m*Y m=Y m) ∧
…

    Mentions: OAI.GAD.IsState, OAI.GAD.mass, OAI.GAD.blockProjection

  7. def OAI.GAD.concatenate line 82
  8. theorem OAI.GAD.gram_concatenate line 86
  9. theorem OAI.GAD.mass_concatenate line 99
  10. theorem OAI.GAD.concatenate_sub line 106
  11. theorem OAI.GAD.concatenate_mass_one line 111
  12. theorem OAI.GAD.orthogonal_factor_entropy line 119