OAI/Analysis/FreeGroupFactor/LocalAutomorphism.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.Generation.word line 15
  2. theorem OAI.FreeGroupFactorMain.Generation.word_of line 18
  3. theorem OAI.FreeGroupFactorMain.Generation.word_inv line 21
  4. theorem OAI.FreeGroupFactorMain.Generation.word_continuous line 27
  5. def OAI.FreeGroupFactorMain.Generation.poly line 38
  6. theorem OAI.FreeGroupFactorMain.Generation.poly_zero line 40
  7. theorem OAI.FreeGroupFactorMain.Generation.poly_add line 41
  8. theorem OAI.FreeGroupFactorMain.Generation.poly_single line 44
  9. theorem OAI.FreeGroupFactorMain.Generation.poly_continuous line 47
  10. theorem OAI.FreeGroupFactorMain.Generation.twoNorm_zero line 54
  11. theorem OAI.FreeGroupFactorMain.Generation.twoNorm_add_le line 57
  12. theorem OAI.FreeGroupFactorMain.Generation.twoNorm_smul line 62
  13. theorem OAI.FreeGroupFactorMain.Generation.twoNorm_mul_sub_le line 66
  14. theorem OAI.FreeGroupFactorMain.Generation.word_twoNorm_bound line 78
  15. theorem OAI.FreeGroupFactorMain.Generation.poly_twoNorm_bound line 107
  16. theorem OAI.FreeGroupFactorMain.generator_haar line 139
  17. theorem OAI.FreeGroupFactorMain.trace_symm line 156
  18. theorem OAI.FreeGroupFactorMain.norm_symm_sub line 162
  19. theorem OAI.FreeGroupFactorMain.twoNorm_symm_sub line 167
  20. theorem OAI.FreeGroupFactorMain.laurentValue_eq_value line 174
  21. theorem OAI.FreeGroupFactorMain.firstCoefficients_norm_le line 177
  22. theorem OAI.FreeGroupFactorMain.one_step_generator_estimate line 185
  23. theorem OAI.FreeGroupFactorMain.one_step_word_estimate line 195
  24. theorem OAI.FreeGroupFactorMain.one_step_from_laurent line 219
  25. theorem OAI.FreeGroupFactorMain.one_step line 257