OAI/InformationTheory/AmplitudeDamping/ThermalEntropy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GAD.thermal line 24
2. theorem OAI.GAD.isState_of_posSemidef_trace_re line 29
3. theorem OAI.GAD.thermal_trace line 36
4. def OAI.GAD.blockSwap line 42
5. theorem OAI.GAD.blockSwap_conj line 48
6. theorem OAI.GAD.thermal_zeroEta_gram line 55
7. theorem OAI.GAD.thermal_zeroEta line 65
8. theorem OAI.GAD.thermal_zeroBeta line 79
9. theorem OAI.GAD.thermal_mix line 106
10. theorem OAI.GAD.thermal_entropy line 120

    Source documentation

    The exact finite-dimensional thermal inequality, including all coefficient boundaries.

    theorem thermal_entropy (X Y : Matrix ι κ ℂ) (hX : mass X = 1) (hY : mass Y = 1)
        {a b c d K : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d)
        (hK : 0 ≤ K) (hs : a+b+c+d=1) (hk : a*d-b*c=K^2) :
        let u := (a+b)*(c+d)-K^2
    …

    Mentions: OAI.GAD.mass