OAI/Analysis/BoundedHochschild/PathStages.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Finite path stages, labelled walks and distinguished fresh letters.

  1. theorem OAI.BoundedHochschild.exists_projection_tails line 36
  2. lemma OAI.BoundedHochschild.mul_eq_zero_of_supports line 73
  3. lemma OAI.BoundedHochschild.orthogonal_blocks_norm_sum_le line 80
  4. lemma OAI.BoundedHochschild.supported_sum_norm_le line 108
  5. lemma OAI.BoundedHochschild.supported_smul_sum_norm_le line 121
  6. lemma OAI.BoundedHochschild.exists_signs_energy line 142
  7. lemma OAI.BoundedHochschild.sign_bounded_energy line 171
  8. lemma OAI.BoundedHochschild.norm_compression_le line 191
  9. theorem OAI.BoundedHochschild.no_normal_small_support_sequence line 199
  10. theorem OAI.BoundedHochschild.normal_two_norm_modulus line 299
  11. theorem OAI.BoundedHochschild.primitive_of_normal_finite_tests line 369
  12. abbrev OAI.HochschildRare.StageAlphabet line 409
  13. def OAI.HochschildRare.stageEmbedding line 411
  14. lemma OAI.HochschildRare.goodPath_label_in_range line 415
  15. theorem OAI.HochschildRare.goodPath_distinguished line 433
  16. lemma OAI.HochschildRare.goodPaths_finite line 456
  17. lemma OAI.HochschildRare.boundedWords_finite line 467