OAI/InformationTheory/AmplitudeDamping/ScalarDeficit.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GAD.blockLambdaPlus line 22
  2. def OAI.GAD.blockLambdaMinus line 25
  3. def OAI.GAD.scalarDeficit line 28
  4. theorem OAI.GAD.blockLambda_properties line 32
  5. def OAI.GAD.deficitSpectrum line 46
  6. def OAI.GAD.deficitSigns line 49
  7. def OAI.GAD.deficitLog line 51
  8. theorem OAI.GAD.deficitSpectrum_nonneg line 54
  9. theorem OAI.GAD.deficitSpectrum_trace line 59
  10. theorem OAI.GAD.deficitSpectrum_entropy line 65
  11. theorem OAI.GAD.deficitSpectrum_log line 70
  12. theorem OAI.GAD.scalarDeficit_weighted_le_of_log_le line 92

    Source documentation

    Finite weighted scalar deficits inherit every pointwise logarithmic comparison.

    theorem scalarDeficit_weighted_le_of_log_le {α : Type u_1} [Fintype α]
    (c x y z : α → ℝ) (hx : ∀ i, 0 ≤ x i) (hy : ∀ i, 0 ≤ y i) (hz : ∀ i, 0 ≤ z i)
    (hlog : ∀ t : ℝ, 0 < t → ∑ i, c i * deficitLog (x i) (y i) (z i) t ≤ 0) :
    ∑ i, c i * scalarDeficit (x i) (y i) (z i) ≤ 0 := by
…

    Mentions: OAI.GAD.deficitLog, OAI.GAD.scalarDeficit

  13. theorem OAI.GAD.blockLogDet_scalar line 109

    Source documentation

    Scalar specialization of the noncommutative logdet function.

    theorem blockLogDet_scalar {q d e : ℝ} (hq : 0 ≤ q) (hd : 0 < d) (he : 0 < e) :
    blockLogDet (Matrix.diagonal (fun _ : Fin 1 ↦ (Real.sqrt q : ℂ)))
      (Matrix.diagonal (fun _ ↦ (d : ℂ))) (Matrix.diagonal (fun _ ↦ (e : ℂ))) =
      Real.log (1 + q/(d*e)) := by
…

    Mentions: OAI.GAD.blockLogDet

  14. theorem OAI.GAD.convexOn_log_one_add_div_mul line 141
  15. theorem OAI.GAD.concaveOn_deficitLog_one line 168
  16. theorem OAI.GAD.concaveOn_scalarDeficit_one line 187
  17. theorem OAI.GAD.deficitLog_mono line 219
  18. theorem OAI.GAD.scalarDeficit_mono line 233
  19. theorem OAI.GAD.scalarDeficit_zero line 245
  20. theorem OAI.GAD.scalarDeficit_homogeneous line 256
  21. theorem OAI.GAD.scalarDeficit_perspective line 271
  22. theorem OAI.GAD.scalarDeficit_superadd line 277
  23. theorem OAI.GAD.scalarDeficit_sum_le line 308