OAI/Analysis/FactorGeneration/SpectralTruncation.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Positivity of the tracial pairing does not require the two positive operators to commute. These estimates will control spectral truncation.

  1. theorem OAI.Generator.Tracial.trace_mul_nonneg line 25
  2. theorem OAI.Generator.Tracial.trace_mul_mono line 33
  3. theorem OAI.Generator.Tracial.trace_mul_le_norm line 39
  4. theorem OAI.Generator.Tracial.norm₂_sub_sq line 48
  5. def OAI.Generator.Tracial.upperTruncate line 70
  6. theorem OAI.Generator.Tracial.upperTruncate_cfc line 73
  7. theorem OAI.Generator.Tracial.upperTruncate_selfAdjoint line 91
  8. theorem OAI.Generator.Tracial.upperTruncate_norm_le line 95
  9. theorem OAI.Generator.Tracial.upperTruncate_discard_mul line 108
  10. theorem OAI.Generator.Tracial.upperTruncate_distance line 123
  11. theorem OAI.Generator.Tracial.included_selfAdjoint line 164
  12. theorem OAI.Generator.Tracial.included_upperTruncate line 169
  13. theorem OAI.Generator.Tracial.selfAdjoint_norm_le_of_bounds line 177
  14. theorem OAI.Generator.Tracial.selfAdjoint_ball_minimum_upper line 194
  15. theorem OAI.Generator.Tracial.selfAdjoint_ball_minimum_norm line 215
  16. def OAI.Generator.Tracial.traceSymmetrize line 246
  17. theorem OAI.Generator.Tracial.traceSymmetrize_selfAdjoint line 249
  18. theorem OAI.Generator.Tracial.traceSymmetrize_eq_self line 253
  19. theorem OAI.Generator.Tracial.traceSymmetrize_sub line 258
  20. theorem OAI.Generator.Tracial.traceSymmetrize_norm₂_le line 263
  21. def OAI.Generator.Tracial.traceClip line 271
  22. theorem OAI.Generator.Tracial.traceClip_selfAdjoint line 274
  23. theorem OAI.Generator.Tracial.traceClip_cfc line 278
  24. theorem OAI.Generator.Tracial.traceClip_norm_le line 286
  25. theorem OAI.Generator.Tracial.traceClip_distance line 298