OAI/Analysis/OperatorAlgebra/UnitaryMeanProperties.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Linearity, positivity and the fixed points of unitary orbit averaging.

  1. lemma OAI.WeakPureInfiniteness.unitaryOrbitMean_add line 15
  2. lemma OAI.WeakPureInfiniteness.unitaryOrbitMean_smul line 31
  3. def OAI.WeakPureInfiniteness.unitaryOrbitMeanCLM line 47
  4. lemma OAI.WeakPureInfiniteness.unitaryOrbitMean_fix line 56
  5. lemma OAI.WeakPureInfiniteness.unitaryOrbitMean_positive line 72
  6. lemma OAI.WeakPureInfiniteness.unitaryOrbitMean_commutes line 85