OAI/Analysis/Unitarizability/ComplexFrames.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Complexification preserves real synthesis norm bounds. The real and imaginary coefficient vectors are handled separately.

  1. def OAI.Dixmier.ComplexFrames.ofReal line 15
  2. def OAI.Dixmier.ComplexFrames.realPart line 16
  3. def OAI.Dixmier.ComplexFrames.imagPart line 17
  4. theorem OAI.Dixmier.ComplexFrames.ofReal_norm line 19
  5. theorem OAI.Dixmier.ComplexFrames.norm_sq_split line 24
  6. theorem OAI.Dixmier.ComplexFrames.synthesis_realPart line 33
  7. theorem OAI.Dixmier.ComplexFrames.synthesis_imagPart line 41
  8. theorem OAI.Dixmier.ComplexFrames.synthesis_bound line 49