OAI/Analysis/FactorGeneration/MatrixSequence.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix stages and a quantified refinement operation, including zero expectation. Reindexing changes no represented algebra.

  1. structure OAI.Generator.FiniteMatrixStage line 15
  2. def OAI.Generator.FiniteMatrixStage.commutant line 24
  3. theorem OAI.Generator.FiniteMatrixStage.commutant_le line 27
  4. def OAI.Generator.FiniteMatrixStage.energy line 30
  5. theorem OAI.Generator.FiniteMatrixStage.energy_nonneg line 34
  6. theorem OAI.Generator.FiniteMatrixStage.commutant_antitone line 37
  7. theorem OAI.Generator.FiniteMatrixStage.energy_antitone line 42
  8. theorem OAI.Generator.FiniteMatrixStage.exists_refinement_descent line 51
  9. theorem OAI.Generator.FiniteMatrixStage.exists_finite_family_descent line 105
  10. theorem OAI.Generator.FiniteMatrixStage.exists_iterated_energy_descent line 122
  11. theorem OAI.Generator.FiniteMatrixStage.exists_finite_matrix_energy_budget line 139
  12. theorem OAI.Generator.FiniteMatrixStage.exists_countable_matrix_refinement line 169
  13. theorem OAI.Generator.Tracial.exists_countable_norm₂_dense line 215
  14. theorem OAI.Generator.FiniteMatrixStage.scalar_common_commutant_of_dense_energy_decay line 240
  15. theorem OAI.Generator.FiniteMatrixStage.exists_irreducible_matrix_sequence line 277
  16. theorem OAI.Generator.Tracial.vonNeumann_wotClosed line 307
  17. def OAI.Generator.FiniteMatrixStage.generated line 332
  18. theorem OAI.Generator.FiniteMatrixStage.generated_closed line 335
  19. theorem OAI.Generator.FiniteMatrixStage.stage_le_generated line 337
  20. theorem OAI.Generator.FiniteMatrixStage.generated_le line 342
  21. theorem OAI.Generator.FiniteMatrixStage.generated_minimal line 348
  22. theorem OAI.Generator.FiniteMatrixStage.generated_relative_scalar line 356
  23. theorem OAI.Generator.FiniteMatrixStage.concrete_stage_monotone line 372
  24. def OAI.Generator.FiniteMatrixStage.scalarStage line 380
  25. theorem OAI.Generator.FiniteMatrixStage.exists_irreducible_matrix_generated_algebra line 391
  26. theorem OAI.Generator.Tracial.irreducible_subalgebra_isII1 line 423
  27. def OAI.Generator.FiniteMatrixStage.generatedVonNeumann line 447
  28. theorem OAI.Generator.FiniteMatrixStage.generatedVonNeumann_le line 450
  29. def OAI.Generator.FiniteMatrixStage.generatedTrace line 453
  30. theorem OAI.Generator.FiniteMatrixStage.generated_isII1 line 457
  31. theorem OAI.Generator.FiniteMatrixStage.exists_irreducible_matrix_generated_II1 line 470
  32. def OAI.Generator.bicommutantStar line 498
  33. theorem OAI.Generator.bicommutantStar_coe line 502
  34. def OAI.Generator.bicommutantVonNeumann line 508
  35. theorem OAI.Generator.bicommutantVonNeumann_coe line 515
  36. theorem OAI.Generator.wstar_starAlgebra_eq_bicommutant line 520
  37. def OAI.Generator.FiniteMatrixStage.stageUnion line 538
  38. theorem OAI.Generator.FiniteMatrixStage.stageUnion_coe line 541
  39. theorem OAI.Generator.FiniteMatrixStage.generated_eq_wstar_union line 546
  40. theorem OAI.Generator.FiniteMatrixStage.exists_stage_strong_approximation line 552
  41. theorem OAI.Generator.FiniteMatrixStage.exists_stage_norm₂_approximation line 567