OAI/Analysis/KadisonKastler/TracialPartitionRemainder.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The common remainder of rounded spectral pieces

  1. def OAI.KadisonKastler.partitionRemainder line 21

    Source documentation

    All discarded pieces are supported in the complement of the rounded pieces.

    def partitionRemainder : AlgebraProjection M :=
…
  2. def OAI.KadisonKastler.partitionResidual line 26
  3. theorem OAI.KadisonKastler.partitionResidual_le_piece line 30
  4. theorem OAI.KadisonKastler.partitionResidual_total line 35
  5. theorem OAI.KadisonKastler.partitionResidual_le_remainder line 41
  6. theorem OAI.KadisonKastler.partitionRemainder_mem line 52
  7. theorem OAI.KadisonKastler.partitionRemainder_trace line 57

    Source documentation

    The trace of the common remainder is the sum of the discarded traces.

    theorem partitionRemainder_trace (τ : TracialRepresentation M) :
    (τ.trace (partitionRemainder Q q hq).val).re =
      ∑ i, τ.norm₂ ((Q.piece i).val - (q i).val) ^ 2 := by
…

    Mentions: OAI.KadisonKastler.partitionRemainder

  8. theorem OAI.KadisonKastler.partitionRemainder_trace_le line 67