Search results

Questions about definition of a KET

questionFurther information is requestedFurther information is requested

Status: Open.

#18 In Timeroot/Lean-QuantumInfo;

· swiswioo24 opened on Oct 23, 2025

Switch CPTPMap + more to "___Class"

tech-debtThings that "should be" betterThings that "should be" better

Status: Open.

#13 In Timeroot/Lean-QuantumInfo;

· Timeroot opened on Jun 12, 2025

Switch Bra/Ket to use EuclideanSpace

tech-debtThings that "should be" betterThings that "should be" better

Status: Open.

#12 In Timeroot/Lean-QuantumInfo;

· Timeroot opened on Jun 12, 2025

Data Processing Inequality

theorem-wishlist

Status: Open.

#10 In Timeroot/Lean-QuantumInfo;

· Timeroot opened on Jun 12, 2025

Strong Subadditivity

theorem-wishlist

Status: Open.

#9 In Timeroot/Lean-QuantumInfo;

· Timeroot opened on Jun 12, 2025

Subadditivity of von Neumann Entropy

theorem-wishlist

Status: Open.

#8 In Timeroot/Lean-QuantumInfo;

· Timeroot opened on Jun 12, 2025

Mathlib has <code>-x * log x</code> and some things on entropy

Status: Open.

#1 In Timeroot/Lean-QuantumInfo;

· adomasbaliuka opened on Aug 2, 2024