OAI/Analysis/FreeWords/FactorBase.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.KKTraceTransfer.concreteClosed line 124
  2. def OAI.KKTraceTransfer.concreteOrder line 129
  3. def OAI.KKTraceTransfer.concreteLE line 134
  4. def OAI.KKTraceTransfer.concretePreorder line 139
  5. theorem OAI.KKTraceTransfer.concreteSOR line 144
  6. def OAI.KKTraceTransfer.seqOrder line 149
  7. def OAI.KKTraceTransfer.seqLE line 154
  8. def OAI.KKTraceTransfer.seqPreorder line 159
  9. theorem OAI.KKTraceTransfer.seqSOR line 164
  10. def OAI.KKTraceTransfer.tracePositive line 169
  11. def OAI.KKTraceTransfer.operatorSequence line 207
  12. theorem OAI.KKTraceTransfer.operatorSequence_apply line 215
  13. theorem OAI.KKTraceTransfer.norm_operatorSequence_le line 218
  14. def OAI.KKTraceTransfer.sequenceMean line 222
  15. theorem OAI.KKTraceTransfer.norm_sequenceMean_le line 239
  16. theorem OAI.KKTraceTransfer.tendsto_sequenceMean line 243
  17. theorem OAI.KKTraceTransfer.trace_sequenceMean line 249
  18. theorem OAI.KKTraceTransfer.sequenceMean_const line 263
  19. theorem OAI.KKTraceTransfer.sequenceMean_bimodule line 272