OAI/Analysis/BoundedHochschild/PowerRigidity.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Approximate power identities and rigidity for contractions.

  1. def OAI.HochschildRigidity.unitaryHarmonicError line 21
  2. theorem OAI.HochschildRigidity.unitary_power_approx_multiplier_bound line 27
  3. lemma OAI.HochschildRigidity.norm_fourierWindow_le_one line 94
  4. lemma OAI.HochschildRigidity.tendsto_smul_power_error line 108
  5. lemma OAI.HochschildRigidity.tendsto_harmonic_power_error line 119
  6. lemma OAI.HochschildRigidity.tendsto_unitaryHarmonicError line 134
  7. lemma OAI.HochschildRigidity.tendsto_preGNS_mul_zero_of_contraction line 157
  8. lemma OAI.HochschildRigidity.tendsto_harmonic_errorFamily line 168
  9. theorem OAI.HochschildRigidity.unitary_power_rigidity_of_tendsto line 192
  10. lemma OAI.HochschildMatrixDilation.matrixTrace_entry_le line 259
  11. lemma OAI.HochschildMatrixDilation.tendsto_matrixTrace_of_entries line 278
  12. lemma OAI.HochschildMatrixDilation.matrixMap_sequential line 287
  13. lemma OAI.HochschildMatrixDilation.preGNS_norm_pow_sub_le line 302
  14. lemma OAI.HochschildMatrixDilation.diag_pow line 322
  15. lemma OAI.HochschildMatrixDilation.tendsto_multiplier_error_transfer line 327
  16. lemma OAI.HochschildMatrixDilation.tendsto_preGNS_pow_sub line 358
  17. theorem OAI.HochschildMatrixDilation.contraction_power_rigidity line 369