Covering entropy for types in tracial W^*- algebras

by DAVID JEKEL

The first displayed equation in the paper includes the term τ (X₁ * Y * X₂ * Z) ^ 2 Here τ is the trace and * is matrix multiplication. There are two ways to parenthesize this and here we prove their inequivalence. Perhaps it does not matter for the paper, however. In that sense, mathematical articles may be underdetermined without being wrong.

We give examples over ℚ, ℝ, ℂ. Over each we can use the tactic aesop; over ℚ we can also use decide.

def I : Fin 2 → Fin 2 → ℝ

Equations

• I x y = if x = y then 1 else 0

theorem square : I ^ 2 = I

def τ : (Fin 2 → Fin 2 → ℝ) → ℝ

Equations

• τ = Matrix.trace

theorem two : τ I = 2

theorem parentheses_matter : τ I ^ 2 ≠ τ (I ^ 2)

theorem without_parentheses : τ I ^ 2 = τ I ^ 2

Lean's convention is perhaps surprising here:

def Iℚ : Fin 2 → Fin 2 → ℚ

Equations

• Iℚ x y = if x = y then 1 else 0

theorem squareℚ : Iℚ ^ 2 = Iℚ

def τℚ : (Fin 2 → Fin 2 → ℚ) → ℚ

Equations

• τℚ = Matrix.trace

theorem twoℚ : τℚ Iℚ = 2

theorem parentheses_matterℚ : τℚ Iℚ ^ 2 ≠ τℚ (Iℚ ^ 2)

theorem without_parenthesesℚ : τℚ Iℚ ^ 2 = τℚ Iℚ ^ 2

def Iℂ : Fin 2 → Fin 2 → ℂ

Equations

• Iℂ x y = if x = y then 1 else 0

theorem squareℂ : Iℂ ^ 2 = Iℂ

def τℂ : (Fin 2 → Fin 2 → ℂ) → ℂ

Equations

• τℂ = Matrix.trace

theorem twoℂ : τℂ Iℂ = 2

theorem parentheses_matterℂ : τℂ Iℂ ^ 2 ≠ τℂ (Iℂ ^ 2)

theorem without_parenthesesℂ : τℂ Iℂ ^ 2 = τℂ Iℂ ^ 2