OAI/Analysis/KadisonKastler/FiniteAveraging.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite averages of unitary conjugations

  1. def OAI.KadisonKastler.finiteAverage line 17

    Source documentation

    Uniform average over a nonempty finite set.

    def finiteAverage (f : G → V) : V := (Fintype.card G : ℂ)⁻¹ • ∑ g, f g
…
  2. theorem OAI.KadisonKastler.finiteAverage_const line 20
  3. theorem OAI.KadisonKastler.finiteAverage_sub line 24
  4. theorem OAI.KadisonKastler.norm_finiteAverage_le line 28
  5. def OAI.KadisonKastler.finiteUnitaryAverage line 43

    Source documentation

    Average over the image of a finite unitary representation.

    def finiteUnitaryAverage (π : G → unitary (H →L[ℂ] H)) (h : H →L[ℂ] H) : H →L[ℂ] H :=
…
  6. theorem OAI.KadisonKastler.finiteUnitaryAverage_star line 47
  7. theorem OAI.KadisonKastler.finiteUnitaryAverage_selfAdjoint line 52
  8. theorem OAI.KadisonKastler.finiteUnitaryAverage_invariant line 60
  9. theorem OAI.KadisonKastler.finiteUnitaryAverage_commutes line 71
  10. theorem OAI.KadisonKastler.norm_sub_finiteUnitaryAverage_le line 83
  11. theorem OAI.KadisonKastler.commutator_unitaryConj line 102

    Source documentation

    Conjugating a commutator conjugates its argument in the opposite direction.

    theorem commutator_unitaryConj (u : unitary (H →L[ℂ] H)) (h a : H →L[ℂ] H) :
    unitaryConj u h * a - a * unitaryConj u h =
      unitaryConj u (h * unitaryConj (star u) a - unitaryConj (star u) a * h) := by
…

    Mentions: OAI.KadisonKastler.unitaryConj

  12. theorem OAI.KadisonKastler.finiteUnitaryAverage_derivation_le line 110