OAI/Analysis/FactorGeneration/RelativeGeneration.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Actual finite star polynomials in one unitary variable and coefficients in an included von Neumann algebra. Both uniform operator bounds and continuity of trace-vector evaluation are proved by recursion on the expression.

  1. inductive OAI.Generator.RelativePolynomial line 16
  2. def OAI.Generator.Tracial.RelativePolynomial.eval line 30
  3. theorem OAI.Generator.Tracial.RelativePolynomial.norm_bound line 38
  4. def OAI.Generator.Tracial.RelativePolynomial.sectionVector line 63
  5. theorem OAI.Generator.Tracial.RelativePolynomial.continuous_sectionVector line 66
  6. def OAI.Generator.Tracial.relativeGenerators line 101
  7. def OAI.Generator.Tracial.relativeGenerated line 104
  8. theorem OAI.Generator.Tracial.relativeGenerated_le line 108
  9. theorem OAI.Generator.Tracial.le_relativeGenerated line 116
  10. theorem OAI.Generator.Tracial.unitary_mem_relativeGenerated line 119
  11. def OAI.Generator.Tracial.RelativePolynomial.valueAlgebra line 125
  12. theorem OAI.Generator.Tracial.RelativePolynomial.eval_mem line 128
  13. theorem OAI.Generator.Tracial.RelativePolynomial.exists_eval line 138
  14. theorem OAI.Generator.Tracial.RelativePolynomial.valueAlgebra_le line 160
  15. theorem OAI.Generator.Tracial.RelativePolynomial.generated_eq_wstar_values line 164
  16. theorem OAI.Generator.Tracial.RelativePolynomial.exists_vector_approximation line 171
  17. def OAI.Generator.Tracial.relativeTraceSpace line 188
  18. instance OAI.Generator.Tracial.relativeTraceSpace_complete line 191
  19. theorem OAI.Generator.Tracial.polynomialVector_mem line 195
  20. theorem OAI.Generator.Tracial.polynomialVector_dense line 201
  21. def OAI.Generator.Tracial.relativeUnitaryWord line 229
  22. theorem OAI.Generator.Tracial.relativeUnitaryWord_mem_unitary line 235
  23. theorem OAI.Generator.Tracial.relativeUnitaryWord_mem_generated line 246
  24. theorem OAI.Generator.Tracial.norm₂_unitary line 261
  25. theorem OAI.Generator.Tracial.relativeUnitaryWord_correlation_le line 267
  26. theorem OAI.Generator.Tracial.perturbation_size_tendsto line 277
  27. theorem OAI.Generator.Tracial.relative_projection_lowerSemicontinuous line 298
  28. theorem OAI.Generator.Tracial.common_relative_projection_continuity line 306
  29. theorem OAI.Generator.Tracial.common_relative_projection_continuity_algebra line 318
  30. theorem OAI.Generator.Tracial.conditionalExpectation_vector_projection line 331
  31. theorem OAI.Generator.Tracial.exists_unitary_outside line 352
  32. def OAI.Generator.Tracial.subalgebraResidual line 368
  33. theorem OAI.Generator.Tracial.subalgebraResidual_vector line 371
  34. theorem OAI.Generator.Tracial.subalgebraResidual_projection line 377
  35. theorem OAI.Generator.Tracial.subalgebraResidual_correlation line 383
  36. theorem OAI.Generator.Tracial.subalgebraResidual_norm_pos line 392