OAI/Analysis/InterpolatedFactors/OperatorSums.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeGroupFactorMain.Amplification.OperatorSum.Operator line 14
  2. def OAI.FreeGroupFactorMain.Amplification.OperatorSum.IsPartial line 16
  3. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.initial_projection line 18
  4. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.partial_star line 26
  5. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.partial_norm_le line 30
  6. structure OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials line 35
  7. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.adjoint line 40
  8. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.finite_offdiag line 46
  9. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.finite_partial line 55
  10. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.ranges line 70
  11. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.apply_summable line 80
  12. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.tsum_bound line 98
  13. def OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.sum line 109
  14. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.sum_apply line 123
  15. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.sum_star line 134
  16. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.star_single_mul_sum line 150
  17. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.star_sum_mul_single line 162
  18. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.sum_mul_star_single line 167
  19. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.sum_partial line 172
  20. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.sum_mem_centralizer line 182
  21. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.sum_left_support line 204
  22. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.sum_right_support line 213
  23. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.residual_projection line 225
  24. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.sum_final_mul_single line 232
  25. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.OrthogonalPartials.single_mul_sum_initial line 236
  26. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.IsPartial.initial_zero line 241
  27. def OAI.FreeGroupFactorMain.Amplification.OperatorSum.PartialFamily line 246
  28. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.maximal_partial_family line 250
  29. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.PartialFamily.orthogonal line 265
  30. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.commutant_maximal_partial line 276
  31. def OAI.FreeGroupFactorMain.Amplification.Polar.centralSupportSpace line 352
  32. instance OAI.FreeGroupFactorMain.Amplification.Polar.centralSupportSpace_complete line 355
  33. theorem OAI.FreeGroupFactorMain.Amplification.Polar.centralSupportSpace_invariant line 359
  34. theorem OAI.FreeGroupFactorMain.Amplification.Polar.centralSupport_commutes line 372
  35. theorem OAI.FreeGroupFactorMain.Amplification.Polar.centralSupport_mem_centralizer line 382
  36. theorem OAI.FreeGroupFactorMain.Amplification.Polar.centralSupport_fixes line 404
  37. theorem OAI.FreeGroupFactorMain.Amplification.Polar.centralSupport_annihilated line 412
  38. theorem OAI.FreeGroupFactorMain.Amplification.Polar.cross_corner_nonzero line 425
  39. theorem OAI.FreeGroupFactorMain.Amplification.OperatorSum.factor_partial_comparison line 448
  40. theorem OAI.FreeGroupFactorMain.Amplification.projection_inner line 473
  41. theorem OAI.FreeGroupFactorMain.Amplification.partial_initial_norm_sq line 481
  42. theorem OAI.FreeGroupFactorMain.Amplification.orthogonal_projection_norm_sq line 488
  43. theorem OAI.FreeGroupFactorMain.Amplification.stabilizedProjectionTrace_faithful line 502
  44. theorem OAI.FreeGroupFactorMain.Amplification.stabilizedProjectionTrace_initial line 528
  45. theorem OAI.FreeGroupFactorMain.Amplification.stabilizedProjectionTrace_initial_final line 537
  46. theorem OAI.FreeGroupFactorMain.Amplification.stabilizedProjectionTrace_orthogonal_add line 546
  47. theorem OAI.FreeGroupFactorMain.Amplification.finite_trace_equal_projection_of_le line 558
  48. theorem OAI.FreeGroupFactorMain.Amplification.equal_finite_trace_equivalence line 574
  49. theorem OAI.FreeGroupFactorMain.Amplification.infinite_equal_finite_trace_equivalence line 624