OAI/InformationTheory/AmplitudeDamping/LogDetEntropy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GAD.logEntropyPrimitive line 20

   Source documentation

   A finite-spectrum primitive, continuous even at a zero eigenvalue.

   def logEntropyPrimitive (a t : ℝ) : ℝ :=
   …

2. theorem OAI.GAD.logEntropyPrimitive_zero line 23
3. theorem OAI.GAD.continuousOn_logEntropyPrimitive line 27
4. theorem OAI.GAD.hasDerivAt_logEntropyPrimitive line 39
5. theorem OAI.GAD.tendsto_logEntropyPrimitive line 52
6. theorem OAI.GAD.entropy_sum_le_of_log_sum_le line 66
7. def OAI.GAD.logDetShift line 102
8. theorem OAI.GAD.det_unitary_conj line 104
9. theorem OAI.GAD.logDetShift_eq_sum line 113
10. theorem OAI.GAD.entropy_le_of_logDetShift_le line 140

    Source documentation

    Entropy may be compared between unequal matrix sizes by their resolvent determinants.

    theorem entropy_le_of_logDetShift_le {κ : Type u_3} [Fintype κ] [DecidableEq κ]
        {A : Matrix ι ι ℂ} {B : Matrix κ κ ℂ} (hA : A.PosSemidef) (hB : B.PosSemidef)
        (htrace : A.trace.re = B.trace.re)
        (hlog : ∀ r : ℝ, 0 < r → logDetShift r A ≤ logDetShift r B) :
        entropy A ≤ entropy B := by
    …

    Mentions: OAI.GAD.logDetShift, OAI.GAD.entropy

11. theorem OAI.GAD.entropy_eq_of_logDetShift_eq line 168
12. theorem OAI.GAD.entropy_mul_conjTranspose line 177

    Source documentation

    Nonzero spectra, including their entropy, agree for both rectangular Gram matrices.

    theorem entropy_mul_conjTranspose {κ : Type u_5} [Fintype κ] [DecidableEq κ]
        (A : Matrix ι κ ℂ) : entropy (A * Aᴴ) = entropy (Aᴴ * A) := by
    …

    Mentions: OAI.GAD.entropy