OAI/InformationTheory/AmplitudeDamping/EntropyContinuity.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GAD.frobVector line 16
2. theorem OAI.GAD.mass_eq_sum_normSq line 19
3. theorem OAI.GAD.frobVector_norm line 22
4. theorem OAI.GAD.frobVector_add line 27
5. theorem OAI.GAD.frobVector_sub line 29
6. theorem OAI.GAD.frobVector_inner line 31
7. def OAI.GAD.IsProjection line 52
8. theorem OAI.GAD.IsProjection.posSemidef line 55
9. theorem OAI.GAD.IsProjection.complement line 59
10. theorem OAI.GAD.projection_orthogonal line 65
11. theorem OAI.GAD.projection_mass_decomposition line 73
12. theorem OAI.GAD.projection_mass_le line 82
13. theorem OAI.GAD.shannon_le_log_card line 95
14. theorem OAI.GAD.entropy_le_log_card line 113
15. theorem OAI.GAD.state_normalize_trace line 118
16. theorem OAI.GAD.entropy_coupling_bound line 125

    Source documentation

    Entropy continuity from a positive common-mixture coupling.

    theorem entropy_coupling_bound [Nonempty ι] {A B U V : Matrix ι ι ℂ}
        (hA : IsState A) (hB : IsState B) (hU : U.PosSemidef) (hV : V.PosSemidef)
        {t : ℝ} (ht : 0 < t) (htrU : U.trace=(t:ℂ)) (htrV : V.trace=(t:ℂ))
        (heq : A+U=B+V) :
        entropy A-entropy B ≤ t*Real.log (Fintype.card ι)+(1+t)*Real.binEntropy (t/(1+t)) := by
    …

    Mentions: OAI.GAD.IsState, OAI.GAD.entropy

17. theorem OAI.GAD.mass_real_smul line 173
18. theorem OAI.GAD.mass_add line 178
19. theorem OAI.GAD.mass_sub line 184
20. theorem OAI.GAD.gram_posSemidef line 190
21. theorem OAI.GAD.gram_trace line 193
22. theorem OAI.GAD.factor_entropy_bound line 199

    Source documentation

    Quantitative entropy comparison from close normalized Gram factors.

    theorem factor_entropy_bound [Nonempty ι] (X Y : Matrix ι κ ℂ)
        (hX : mass X=1) (hY : mass Y=1) {ε : ℝ} (hε : 0 < ε) :
        entropy (gram X)-entropy (gram Y) ≤
          (mass (X-Y)/(4*ε)+ε)*Real.log (Fintype.card ι)+
            (1+mass (X-Y)/(4*ε)+ε)*Real.log 2 := by
    …

    Mentions: OAI.GAD.mass, OAI.GAD.entropy, OAI.GAD.gram

23. theorem OAI.GAD.mass_eq_zero line 277
24. theorem OAI.GAD.projection_inner line 283
25. theorem OAI.GAD.exists_projected_factor line 291

    Source documentation

    Normalize a successful projection without losing more than twice its failure mass.

    theorem exists_projected_factor {P : Matrix ι ι ℂ} (hP : IsProjection P)
        (X B : Matrix ι κ ℂ) (hX : mass X=1) (hB : mass B=1) (hPB : P*B=B) :
        ∃ Y : Matrix ι κ ℂ, mass Y=1 ∧ P*Y=Y ∧ mass (X-Y) ≤ 2*(1-mass (P*X)) := by
    …

    Mentions: OAI.GAD.IsProjection, OAI.GAD.mass