OAI/Analysis/FreeWords/ProjectionRound.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKProjectionSupport.partial_matrix_system_diagonal line 38
  2. theorem OAI.KKProjectionSupport.subprojections_orthogonal line 100
  3. theorem OAI.KKProjectionSupport.orthogonal_sum_projection line 110
  4. theorem OAI.KKProjectionSupport.round_projection_partition line 124
  5. theorem OAI.KKTraceTransfer.traceNorm_eq_gns line 201
  6. theorem OAI.KKTraceTransfer.traceNorm_nonneg line 206
  7. theorem OAI.KKTraceTransfer.traceNorm_add_le line 209
  8. theorem OAI.KKTraceTransfer.traceNorm_mul_le line 214
  9. theorem OAI.KKTraceTransfer.traceNorm_one line 221
  10. theorem OAI.KKTraceTransfer.traceNorm_le_norm line 225
  11. theorem OAI.KKTraceTransfer.traceNorm_projection_sq line 229