OAI/Analysis/TracialSplitting/ProjectionSampling.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentMain.trace_norm_projection_mul_le line 22
  2. lemma OAI.CurrentMain.trace_compression_error line 33
  3. lemma OAI.CurrentMain.scalar_splitting_error line 52
  4. theorem OAI.CurrentMain.split_finite_linear_tests line 83
  5. lemma OAI.CurrentMain.trace_mul_mono_right line 165
  6. lemma OAI.CurrentMain.trace_mul_mono_left line 171
  7. lemma OAI.CurrentMain.trace_projection_difference_sq line 176
  8. lemma OAI.CurrentMain.projection_difference_linear line 186
  9. lemma OAI.CurrentMain.projection_insert_normalized line 224
  10. theorem OAI.CurrentMain.orthogonal_insertion line 271
  11. structure OAI.CurrentMain.ProjectionRow line 332
  12. lemma OAI.CurrentMain.ProjectionRow.right_support line 342
  13. lemma OAI.CurrentMain.ProjectionRow.left_support line 345
  14. def OAI.CurrentMain.ProjectionRow.coeff line 349
  15. lemma OAI.CurrentMain.ProjectionRow.coeff_star line 351
  16. lemma OAI.CurrentMain.ProjectionRow.coeff_mul line 354
  17. def OAI.CurrentMain.ProjectionRow.sample line 368
  18. def OAI.CurrentMain.ProjectionRow.matrix line 370
  19. lemma OAI.CurrentMain.ProjectionRow.sample_star line 372
  20. lemma OAI.CurrentMain.ProjectionRow.sample_mul line 375
  21. lemma OAI.CurrentMain.ProjectionRow.sample_projection line 381
  22. lemma OAI.CurrentMain.ProjectionRow.range_projection line 389
  23. lemma OAI.CurrentMain.ProjectionRow.sample_le line 392
  24. lemma OAI.CurrentMain.ProjectionRow.matrix_star line 399
  25. lemma OAI.CurrentMain.ProjectionRow.matrix_mul line 405
  26. lemma OAI.CurrentMain.ProjectionRow.matrix_one line 431
  27. lemma OAI.CurrentMain.ProjectionRow.sample_matrix line 435
  28. lemma OAI.CurrentMain.ProjectionRow.matrix_sample line 440
  29. lemma OAI.CurrentMain.ProjectionRow.trace_coeff line 445
  30. lemma OAI.CurrentMain.ProjectionRow.trace_sample line 454
  31. lemma OAI.CurrentMain.ProjectionRow.trace_matrix line 460
  32. lemma OAI.CurrentMain.ProjectionRow.matrix_sample_commute line 465
  33. lemma OAI.CurrentMain.proportional_complex_bound line 477
  34. lemma OAI.CurrentMain.norm_square_difference line 508
  35. lemma OAI.CurrentMain.trace_supported_norm_le line 519
  36. lemma OAI.CurrentMain.sampling_compression_estimates line 524
  37. lemma OAI.CurrentMain.complex_difference_transfer line 595
  38. lemma OAI.CurrentMain.real_difference_transfer line 603
  39. lemma OAI.CurrentMain.sampling_via_scalar_reference line 613
  40. lemma OAI.CurrentMain.ProjectionRow.trace_matrix_proportion line 699
  41. theorem OAI.CurrentMain.ProjectionRow.matrix_block_sampling line 707