OAI/Analysis/FactorGeneration/ProjectionLimits.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

A nonzero projection in a diffuse tracial algebra contains nonzero projections of arbitrarily small trace.

  1. theorem OAI.Generator.Tracial.projection_trace_sq line 20
  2. theorem OAI.Generator.Tracial.projection_trace_pos line 26
  3. theorem OAI.Generator.Tracial.exists_half_trace_subprojection line 31
  4. theorem OAI.Generator.Tracial.exists_geometric_trace_subprojection line 48
  5. theorem OAI.Generator.Tracial.exists_small_trace_subprojection line 69
  6. def OAI.Generator.Tracial.AlgebraProjection line 95

    Source documentation

    Projections with their algebraic range-inclusion order.

    def AlgebraProjection (M : VonNeumannAlgebra H) :=
…
  7. instance OAI.Generator.Tracial.algebraProjectionPartialOrder line 98
  8. theorem OAI.Generator.Tracial.projection_mul_of_le line 112
  9. theorem OAI.Generator.Tracial.monotone_projection_upper_bound line 120

    Source documentation

    A bounded increasing net of actual projections has a projection upper bound with the same trace bound. No projection-lattice completeness is assumed.

    theorem monotone_projection_upper_bound (τ : TracialRepresentation M)
    {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (a : ι → AlgebraProjection M) (ha : Monotone a) (r : ℝ)
    (hr : ∀ i, (τ.trace (a i).val).re ≤ r) :
    ∃ b : AlgebraProjection M, (∀ i, a i ≤ b) ∧ (τ.trace b.val).re ≤ r ∧
      ∀ p : AlgebraProjection M, (∀ i, a i ≤ p) → b ≤ p := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection

  10. theorem OAI.Generator.Tracial.exists_maximal_trace_subprojection line 204
  11. theorem OAI.Generator.Tracial.exists_exact_trace_subprojection line 230

    Source documentation

    Every projection can be cut to any smaller prescribed real trace.

    theorem exists_exact_trace_subprojection
    (hdiff : ∀ p : M.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q : M.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p*q = q ∧ q*p = q)
    (p : M.toStarSubalgebra) (hp : IsStarProjection p)
    (r : ℝ) (hr : 0 ≤ r) (hrp : r ≤ (τ.trace p).re) :
    ∃ q : M.toStarSubalgebra, IsStarProjection q ∧ p*q = q ∧ q*p = q ∧
      τ.trace q = (r : ℂ) := by
…
  12. structure OAI.Generator.Tracial.CornerUnitary line 297

    Source documentation

    An actual operator with identical initial and final support p.

    structure CornerUnitary (p : AlgebraProjection M) where
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection

  13. theorem OAI.Generator.Tracial.CornerUnitary.mul_support line 305
  14. theorem OAI.Generator.Tracial.CornerUnitary.support_mul line 313
  15. def OAI.Generator.Tracial.CornerUnitary.adjoint line 318
  16. theorem OAI.Generator.Tracial.CornerUnitary.mul_eq_zero line 322
  17. def OAI.Generator.Tracial.CornerUnitary.patch line 328
  18. theorem OAI.Generator.Tracial.CornerUnitary.patch_extends line 348
  19. theorem OAI.Generator.Tracial.CornerUnitary.norm_sq line 360
  20. theorem OAI.Generator.Tracial.CornerUnitary.norm_le_one line 363
  21. theorem OAI.Generator.Tracial.CornerUnitary.trace_norm_sq line 368
  22. theorem OAI.Generator.Tracial.CornerUnitary.patch_trace_increases line 374
  23. def OAI.Generator.Tracial.DyadicIndex line 395

    Source documentation

    At depth n there are 2^n indices; a successor appends a binary branch.

    def DyadicIndex : ℕ → Type
  | 0 => Unit
  | n+1 => DyadicIndex n × Bool
  24. instance OAI.Generator.Tracial.dyadicIndexFintype line 399
  25. instance OAI.Generator.Tracial.dyadicIndexDecidableEq line 403
  26. theorem OAI.Generator.Tracial.card_dyadicIndex line 405
  27. theorem OAI.Generator.Tracial.exists_half_trace_cut line 414
  28. def OAI.Generator.Tracial.halfTraceCut line 423
  29. theorem OAI.Generator.Tracial.halfTraceCut_le line 426
  30. theorem OAI.Generator.Tracial.halfTraceCut_trace line 429
  31. def OAI.Generator.Tracial.splitProjection line 434

    Source documentation

    Both halves belong to the original algebra.

    def splitProjection (p : AlgebraProjection M) (b : Bool) : AlgebraProjection M :=
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection

  32. theorem OAI.Generator.Tracial.splitProjection_le line 439
  33. theorem OAI.Generator.Tracial.splitProjection_sum line 446
  34. theorem OAI.Generator.Tracial.splitProjection_orthogonal line 450
  35. theorem OAI.Generator.Tracial.splitProjection_trace line 456
  36. def OAI.Generator.Tracial.dyadicProjection line 472
  37. theorem OAI.Generator.Tracial.dyadicProjection_le_parent line 476
  38. theorem OAI.Generator.Tracial.dyadicProjection_trace line 480
  39. theorem OAI.Generator.Tracial.dyadicProjection_sum line 489
  40. theorem OAI.Generator.Tracial.orthogonal_subprojections line 499
  41. theorem OAI.Generator.Tracial.dyadicProjection_orthogonal line 505
  42. def OAI.Generator.Tracial.coordinateTraceLinear line 534
  43. theorem OAI.Generator.Tracial.projection_trace_real line 539
  44. def OAI.Generator.Tracial.projectionSum line 547
  45. theorem OAI.Generator.Tracial.projectionSum_star line 550
  46. theorem OAI.Generator.Tracial.projectionSum_mul line 554
  47. theorem OAI.Generator.Tracial.projectionSum_trace line 569
  48. abbrev OAI.Generator.Tracial.dyadicEval line 582
  49. theorem OAI.Generator.Tracial.dyadicEval_one line 585
  50. theorem OAI.Generator.Tracial.dyadicEval_refine line 589
  51. theorem OAI.Generator.Tracial.dyadicEval_lift line 598
  52. theorem OAI.Generator.Tracial.dyadicEval_trace line 607