OAI/Analysis/BoundedHochschild/IncrementalPatching.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Corner partial unitaries, incremental moment estimates and unitary completion.

  1. def OAI.HochschildPatching.ofCornerUnitary line 40
  2. lemma OAI.HochschildPatching.ofCornerUnitary_coe line 49
  3. lemma OAI.HochschildPatching.ofCornerUnitary_support line 51
  4. lemma OAI.HochschildPatching.corner_coe_pow_succ line 55
  5. def OAI.HochschildPatching.signedExponent line 62
  6. lemma OAI.HochschildPatching.signedExponent_ne_zero line 63
  7. lemma OAI.HochschildPatching.ofCornerUnitary_power line 65
  8. theorem OAI.HochschildPatching.exists_partial_unitary_weak_powers line 79
  9. lemma OAI.HochschildPatching.exists_incremental_patch line 129
  10. def OAI.HochschildPatching.expBudget line 193
  11. lemma OAI.HochschildPatching.expBudget_zero line 194
  12. lemma OAI.HochschildPatching.expBudget_continuous line 195
  13. lemma OAI.HochschildPatching.expBudget_nonneg line 196
  14. lemma OAI.HochschildPatching.expBudget_increment line 198
  15. def OAI.HochschildPatching.patchRate line 206
  16. def OAI.HochschildPatching.patchTolerance line 207
  17. lemma OAI.HochschildPatching.patchRate_ge_one line 208
  18. lemma OAI.HochschildPatching.patchTolerance_pos line 212
  19. lemma OAI.HochschildPatching.patch_slope_bound line 216
  20. lemma OAI.HochschildPatching.expBudget_patch_bound line 239
  21. theorem OAI.HochschildPatching.exists_partial_unitary_moments line 264
  22. lemma OAI.HochschildPatching.trace_supported_insertion line 327
  23. lemma OAI.HochschildPatching.trace_wordProduct_patch line 337
  24. lemma OAI.HochschildPatching.trace_mixedEval_patch line 367
  25. def OAI.HochschildPatching.unitaryCompletion line 377