OAI/Analysis/FactorGeneration/PerturbationBounds.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Exact 2 ell signed coefficients in each formal row. In particular the identity prefix label is still a nonidentity basis letter in the formal group.

  1. theorem OAI.Generator.pairLabel_right_injective line 18
  2. def OAI.Generator.rowSignedWord line 27
  3. theorem OAI.Generator.rowSignedWord_injective line 30
  4. theorem OAI.Generator.finitePerturbationRow_signed line 36
  5. theorem OAI.Generator.finitePerturbationRow_norm_sq line 45
  6. theorem OAI.Generator.Tracial.quotient_norm_unitary_mul line 81
  7. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.commonPerturbation_norm_sq line 87
  8. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.commonPerturbation_norm line 109
  9. def OAI.Generator.Tracial.traceVectorCLM line 132
  10. theorem OAI.Generator.Tracial.norm₂_exp_sub_one_le line 140
  11. theorem OAI.Generator.Tracial.norm₂_exp_mul_sub_le line 163
  12. def OAI.Generator.Tracial.unitaryCoordinate line 185
  13. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.retainedUnitary line 189
  14. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbedUnitary_apply line 193
  15. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbedUnitary_distance line 201
  16. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbedWord_apply line 210
  17. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.select_perturbation_coordinate line 226
  18. theorem OAI.Generator.Tracial.exists_represented_perturbation line 278