OAI/Analysis/OperatorAlgebra/UnitaryOrbitMean.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Averaging a strongly continuous unitary orbit using the concrete symmetric-interval mean. The operator is reconstructed from its bounded matrix coefficients; no normality of the averaging map is asserted.

  1. def OAI.WeakPureInfiniteness.unitaryOrbitCoefficient line 18
  2. lemma OAI.WeakPureInfiniteness.unitaryOrbitCoefficient_apply line 31
  3. lemma OAI.WeakPureInfiniteness.unitaryOrbitCoefficient_norm_le line 35
  4. def OAI.WeakPureInfiniteness.unitaryMeanForm line 44
  5. lemma OAI.WeakPureInfiniteness.unitaryMeanForm_add_right line 48
  6. lemma OAI.WeakPureInfiniteness.unitaryMeanForm_smul_right line 59
  7. lemma OAI.WeakPureInfiniteness.unitaryMeanForm_bound line 69
  8. def OAI.WeakPureInfiniteness.unitaryMeanFunctional line 76
  9. def OAI.WeakPureInfiniteness.unitaryMeanLinear line 85
  10. def OAI.WeakPureInfiniteness.unitaryOrbitMean line 109
  11. lemma OAI.WeakPureInfiniteness.unitaryOrbitMean_inner line 116
  12. lemma OAI.WeakPureInfiniteness.unitaryOrbitMean_norm_le line 122