OAI/Analysis/InterpolatedFactors/FiniteCorners.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.Amplification.stabilizationDelta line 15
  2. theorem OAI.FreeGroupFactorMain.Amplification.finite_weight_summable line 19
  3. theorem OAI.FreeGroupFactorMain.Amplification.finite_weight_left_mul line 24
  4. theorem OAI.FreeGroupFactorMain.Amplification.finite_weight_star line 36
  5. theorem OAI.FreeGroupFactorMain.Amplification.finite_weight_toReal line 41
  6. theorem OAI.FreeGroupFactorMain.Amplification.stabilizedTrace_star_mul line 49
  7. theorem OAI.FreeGroupFactorMain.Amplification.stabilizedTrace_star_mul_comm line 66
  8. theorem OAI.FreeGroupFactorMain.Amplification.corner_diag_bound line 74
  9. theorem OAI.FreeGroupFactorMain.Amplification.corner_diag_summable line 98
  10. def OAI.FreeGroupFactorMain.Amplification.finiteCornerTraceLinear line 106
  11. theorem OAI.FreeGroupFactorMain.Amplification.finite_weight_corner line 129
  12. theorem OAI.FreeGroupFactorMain.Amplification.quadratic_polarization line 139
  13. theorem OAI.FreeGroupFactorMain.Amplification.linearMap_ext_star_mul line 148
  14. def OAI.FreeGroupFactorMain.operatorSequenceMap line 163
  15. theorem OAI.FreeGroupFactorMain.ultraweak_mul_conjugate line 167
  16. theorem OAI.FreeGroupFactorMain.groupUltraweak_mul_conjugate line 191
  17. theorem OAI.FreeGroupFactorMain.Amplification.equivalentCorner_finite_trace line 205
  18. theorem OAI.FreeGroupFactorMain.Amplification.equivalentCorner_normalized_finite_trace line 237
  19. theorem OAI.FreeGroupFactorMain.Amplification.stabilizationUltraweak_mul_conjugate line 247
  20. theorem OAI.FreeGroupFactorMain.Amplification.finite_corner_choice_independence line 255