OAI/Analysis/BoundedHochschild/FirstLetter.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite and countable first-letter rigidity for free Haar families.

  1. lemma OAI.HochschildFirstLetter.tendsto_norm_of_span line 20
  2. lemma OAI.HochschildFirstLetter.choose_diagonal line 42
  3. lemma OAI.HochschildFirstLetter.diagonal_error_tendsto line 66
  4. theorem OAI.HochschildFirstLetter.finite_config_rigidity line 80
  5. lemma OAI.HochschildFirstLetter.toWord_map_injective line 143
  6. theorem OAI.HochschildFirstLetter.countable_first_letter_rigidity line 154