OAI/Analysis/FactorGeneration/MatrixExpectation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Construct contractive expectations onto the actual finite matrix stages. For every element of their weak closure, these expectations converge in L2 and remain in its operator norm ball.

  1. theorem OAI.Generator.Tracial.conditionalExpectation_best_approximation line 19
  2. def OAI.Generator.FiniteMatrixStage.stageVonNeumann line 38
  3. theorem OAI.Generator.FiniteMatrixStage.stageVonNeumann_le line 41
  4. def OAI.Generator.FiniteMatrixStage.stageExpectation line 44
  5. theorem OAI.Generator.FiniteMatrixStage.stageExpectation_mem line 48
  6. theorem OAI.Generator.FiniteMatrixStage.stageExpectation_norm_le line 53
  7. theorem OAI.Generator.FiniteMatrixStage.stageExpectation_norm₂_tendsto line 57
  8. theorem OAI.Generator.FiniteMatrixStage.exists_bounded_stage_approximation line 73
  9. theorem OAI.Generator.Tracial.exists_scalar_pinching_for_matrixUnits line 92
  10. theorem OAI.Generator.FiniteMatrixStage.exists_matrix_approximated_centered_partition line 124
  11. def OAI.Generator.FiniteMatrixStage.restrictStage line 161

    Source documentation

    View the same finite matrix stage inside any algebra containing it.

    def restrictStage (E : FiniteMatrixStage N) (R : VonNeumannAlgebra H)
    (hER : E.units.concreteAlgebra ≤ R.toStarSubalgebra) : FiniteMatrixStage R where
…

    Mentions: OAI.Generator.FiniteMatrixStage

  12. theorem OAI.Generator.FiniteMatrixStage.restrictStage_concreteAlgebra line 182
  13. theorem OAI.Generator.FiniteMatrixStage.exists_matrix_generated_centered_partition line 198
  14. theorem OAI.Generator.FiniteMatrixStage.stage_vector_range_separable line 229
  15. theorem OAI.Generator.FiniteMatrixStage.generated_vector_range_separable line 234
  16. theorem OAI.Generator.FiniteMatrixStage.generated_norm₂_separable line 249
  17. theorem OAI.Generator.FiniteMatrixStage.stageExpectation_strong_tendsto line 267
  18. theorem OAI.Generator.FiniteMatrixStage.stageExpectation_strong_star_tendsto line 277
  19. theorem OAI.Generator.FiniteMatrixStage.exists_bounded_strong_stage_approximation line 287
  20. theorem OAI.Generator.FiniteMatrixStage.generated_cyclicSpace_separable line 300