OAI/Analysis/FreeWords/UltraExpectationFull.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKTraceTransfer.linearSurjDescend line 274
  2. theorem OAI.KKTraceTransfer.linearSurjDescend_apply line 280
  3. theorem OAI.KKTraceTransfer.linearSurjDescend_starAlgHom_apply line 288
  4. def OAI.KKTraceTransfer.linearSurjDescendStarAlgHomWithSpec line 295
  5. def OAI.KKTraceTransfer.ultraExpectationLinearWithSpec line 303
  6. def OAI.KKTraceTransfer.ultraExpectationLinear line 311
  7. theorem OAI.KKTraceTransfer.ultraExpectationLinear_projection line 315
  8. theorem OAI.KKTraceTransfer.contractive_descend line 320
  9. theorem OAI.KKTraceTransfer.contractive_descend_cstar line 335
  10. theorem OAI.KKTraceTransfer.ultraExpectationLinear_norm_le line 345
  11. def OAI.KKTraceTransfer.ultraExpectation line 353
  12. theorem OAI.KKTraceTransfer.ultraExpectation_projection line 358
  13. theorem OAI.KKTraceTransfer.descend_bimodule line 363
  14. theorem OAI.KKTraceTransfer.descend_square line 373
  15. theorem OAI.KKTraceTransfer.ultraExpectation_bimodule line 382
  16. theorem OAI.KKTraceTransfer.ultraExpectation_square line 390
  17. theorem OAI.KKTraceTransfer.descend_trace line 401
  18. theorem OAI.KKTraceTransfer.ultraQuotientState_projection line 410
  19. theorem OAI.KKTraceTransfer.ultraExpectation_trace line 416
  20. theorem OAI.KKTraceTransfer.ultra_expectation_exists line 426