OAI/Analysis/TracialSplitting/RowEstimates.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentMain.ProjectionRow.entry_norm_le line 23
  2. lemma OAI.CurrentMain.ProjectionRow.range_eq_sum line 30
  3. lemma OAI.CurrentMain.ProjectionRow.compression_expand line 34
  4. lemma OAI.CurrentMain.ProjectionRow.compression_norm_le line 45
  5. lemma OAI.CurrentMain.selfAdjoint_covariance line 71
  6. lemma OAI.CurrentMain.traceOneNorm_covariance_difference line 75
  7. lemma OAI.CurrentMain.traceOneNorm_sum_le line 108
  8. lemma OAI.CurrentMain.row_covariance_trace_error line 117
  9. lemma OAI.CurrentMain.rowPair_perturb line 139
  10. lemma OAI.CurrentMain.rowPair_real_scale line 159
  11. lemma OAI.CurrentMain.rowPair_scale_error line 165
  12. theorem OAI.CurrentMain.normalize_weighted_row line 181
  13. lemma OAI.CurrentMain.normalized_rowPair_error line 239
  14. def OAI.CurrentMain.ProjectionRow.subrow line 274
  15. def OAI.CurrentMain.ProjectionRow.atom line 281
  16. lemma OAI.CurrentMain.ProjectionRow.atom_eq_coeff line 284
  17. lemma OAI.CurrentMain.ProjectionRow.atom_projection line 288
  18. lemma OAI.CurrentMain.ProjectionRow.atom_orthogonal line 299
  19. lemma OAI.CurrentMain.ProjectionRow.atom_sum line 306
  20. lemma OAI.CurrentMain.ProjectionRow.subrow_range line 308
  21. lemma OAI.CurrentMain.ProjectionRow.upper_cut_subrow line 312
  22. lemma OAI.CurrentMain.ProjectionRow.atom_trace line 324
  23. lemma OAI.CurrentMain.ProjectionRow.atom_nonzero line 330
  24. lemma OAI.CurrentMain.rowPair_spectral_rotation line 346
  25. lemma OAI.CurrentMain.traceOneNorm_of_nonneg line 370
  26. lemma OAI.CurrentMain.covariance_trace_le_of_gram line 375
  27. lemma OAI.CurrentMain.covariance_nonneg line 391
  28. lemma OAI.CurrentMain.covariance_selfAdjoint line 394
  29. lemma OAI.CurrentMain.dropped_covariance_trace line 397
  30. lemma OAI.CurrentMain.covariance_retain_error line 411
  31. theorem OAI.CurrentMain.normalize_retained_spectrum line 448
  32. lemma OAI.CurrentMain.covariance_scaled_row line 482
  33. lemma OAI.CurrentMain.retained_spectrum_trace_error line 492
  34. def OAI.CurrentMain.rawRow line 528
  35. lemma OAI.CurrentMain.rawRow_support line 532
  36. lemma OAI.CurrentMain.rawRow_pair line 537
  37. lemma OAI.CurrentMain.rawRow_covariance line 545
  38. lemma OAI.CurrentMain.rawRow_norm_le_sqrt line 557
  39. lemma OAI.CurrentMain.rawRow_norm_squares line 565
  40. lemma OAI.CurrentMain.rawRow_norm_le_one line 574
  41. lemma OAI.CurrentMain.rawRow_norm_sum line 582
  42. lemma OAI.CurrentMain.rawRow_pair_scalar_error line 589