OAI/Analysis/InterpolatedFactors/Stabilization.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.InfiniteICC.reduced_append_fresh line 14
  2. theorem OAI.FreeGroupFactorMain.InfiniteICC.reduced_conjugate_fresh line 29
  3. theorem OAI.FreeGroupFactorMain.InfiniteICC.conjugate_word line 39
  4. theorem OAI.FreeGroupFactorMain.InfiniteICC.infinite_conjugates line 51
  5. theorem OAI.FreeGroupFactorMain.central_coefficient_conjugate line 71
  6. theorem OAI.FreeGroupFactorMain.group_center_scalar_of_infinite_conjugates line 84
  7. theorem OAI.FreeGroupFactorMain.infinite_free_group_center_scalar line 117
  8. def OAI.FreeGroupFactorMain.Amplification.equivalentCorner line 129
  9. theorem OAI.FreeGroupFactorMain.Amplification.equivalentCorner_trace line 179
  10. theorem OAI.FreeGroupFactorMain.Amplification.equivalentCorner_normal line 187
  11. def OAI.FreeGroupFactorMain.Amplification.contractionFamilyValue line 211
  12. theorem OAI.FreeGroupFactorMain.Amplification.contractionFamilyValue_norm_le line 216
  13. def OAI.FreeGroupFactorMain.Amplification.contractionFamily line 222
  14. theorem OAI.FreeGroupFactorMain.Amplification.contractionFamily_apply line 230
  15. theorem OAI.FreeGroupFactorMain.Amplification.contractionFamily_star line 233
  16. theorem OAI.FreeGroupFactorMain.Amplification.contractionFamily_projection line 249
  17. def OAI.FreeGroupFactorMain.Amplification.productFamily line 263
  18. theorem OAI.FreeGroupFactorMain.Amplification.productFamily_apply line 266
  19. theorem OAI.FreeGroupFactorMain.Amplification.productFamily_projection line 272
  20. theorem OAI.FreeGroupFactorMain.Amplification.productFamily_mem_stabilization line 278
  21. def OAI.FreeGroupFactorMain.Amplification.productSingle line 312
  22. theorem OAI.FreeGroupFactorMain.Amplification.productSingle_apply line 317
  23. def OAI.FreeGroupFactorMain.Amplification.matrixEntry line 322
  24. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_apply line 327
  25. theorem OAI.FreeGroupFactorMain.Amplification.productSingle_single line 332
  26. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_ext line 340
  27. theorem OAI.FreeGroupFactorMain.Amplification.productAmplification_productSingle line 351
  28. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_diagonal_mul line 364
  29. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_mul_diagonal line 372
  30. theorem OAI.FreeGroupFactorMain.Amplification.mem_stabilization_iff_matrix line 381
  31. def OAI.FreeGroupFactorMain.Amplification.productCoordinate line 405
  32. theorem OAI.FreeGroupFactorMain.Amplification.productCoordinate_apply line 409
  33. def OAI.FreeGroupFactorMain.Amplification.matrixUnit line 412
  34. theorem OAI.FreeGroupFactorMain.Amplification.matrixUnit_apply line 415
  35. theorem OAI.FreeGroupFactorMain.Amplification.matrixUnit_productSingle line 419
  36. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_matrixUnit_mul line 432
  37. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_mul_matrixUnit line 440
  38. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_matrixUnit line 448
  39. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_productAmplification line 456
  40. theorem OAI.FreeGroupFactorMain.Amplification.matrixUnit_mem_stabilization line 466
  41. theorem OAI.FreeGroupFactorMain.Amplification.diagonal_mem_stabilization line 474
  42. theorem OAI.FreeGroupFactorMain.Amplification.stabilization_center_diagonal line 483
  43. theorem OAI.FreeGroupFactorMain.Amplification.stabilization_center_scalar line 503
  44. theorem OAI.FreeGroupFactorMain.Amplification.stabilization_center_projection line 527
  45. theorem OAI.FreeGroupFactorMain.Amplification.infinite_stabilization_center_projection line 551
  46. theorem OAI.FreeGroupFactorMain.Amplification.hilbert_ofReal_norm_sq line 560
  47. theorem OAI.FreeGroupFactorMain.Amplification.productSingle_inner_right line 566
  48. theorem OAI.FreeGroupFactorMain.Amplification.productSingle_inner_left line 574
  49. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_star line 581
  50. theorem OAI.FreeGroupFactorMain.Amplification.stabilizedProjectionTrace_eq_matrix line 596
  51. theorem OAI.FreeGroupFactorMain.Amplification.groupVN_adjoint_delta_norm line 614
  52. theorem OAI.FreeGroupFactorMain.Amplification.stabilizedProjectionTrace_star line 627