OAI/Analysis/FactorGeneration/WordCorrelation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Ordered prefix cancellation for the actual common perturbed unitary. All identities are identities of bounded coordinate sequences.

  1. theorem OAI.Generator.prefixes_append_single line 14
  2. theorem OAI.Generator.evaluated_prefixes line 20
  3. theorem OAI.Generator.interleaved_terminal line 33

    Source documentation

    The terminal letter is unperturbed; the same h occurs before every u.

    theorem interleaved_terminal (t : ℕ → G) (u h : G) (n : ℕ) :
    let s : ℕ → G := fun k => if k=0 then t 0 else u*t k
…
  4. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbedWord line 58
  5. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinatePrefix_terminal line 63
  6. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbedWord_prefixes line 74
  7. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.exponential_product_eq_word line 96
  8. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.label_star_trace line 124
  9. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.conjugate_positive_correlation line 135
  10. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.conjugate_negative_correlation line 158
  11. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.firstOrderTerm line 168
  12. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.firstOrder_correlation line 174
  13. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.linearized_correlation line 198
  14. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbationMap_firstOrder line 221
  15. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinate_linearized_correlation line 254
  16. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.exponential_product_correlation line 281
  17. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinatePrefix_quotient line 308
  18. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbedWord_correlation line 315