OAI/Analysis/FactorGeneration/NormalDimension.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Increasing projection suprema and compatible sequential comparison. The witnesses live in the original algebra; no trace or dimension is used.

  1. theorem OAI.Generator.Tracial.AlgebraProjection.exists_isLUB_monotone line 20

    Source documentation

    Actual least upper bounds for arbitrary nonempty directed projection nets.

    theorem exists_isLUB_monotone
    {I : Type*} [Preorder I] [IsDirected I (· ≤ ·)] [Nonempty I]
    (q : I → AlgebraProjection M) (hq : Monotone q) :
    ∃ p : AlgebraProjection M, IsLUB (Set.range q) p := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection

  2. theorem OAI.Generator.Tracial.PartialIsometry.exists_extension_of_subequivalent line 41

    Source documentation

    Extend a given embedding to a larger source while keeping its target in r.

    theorem exists_extension_of_subequivalent (v : PartialIsometry M)
    (p r : AlgebraProjection M) (hp : v.support ≤ p) (hr : v.target ≤ r)
    (hpr : p.Subequivalent r) :
    ∃ w : PartialIsometry M, v ≤ w ∧ w.support=p ∧ w.target ≤ r := by
…

    Mentions: OAI.Generator.Tracial.PartialIsometry, OAI.Generator.Tracial.AlgebraProjection

  3. theorem OAI.Generator.Tracial.PartialIsometry.exists_monotone_embeddings line 65

    Source documentation

    A sequence of comparable sources admits compatible actual embeddings.

    theorem exists_monotone_embeddings (q : ℕ → AlgebraProjection M) (hq : Monotone q)
    (r : AlgebraProjection M) (hr : ∀ n, (q n).Subequivalent r) :
    ∃ a : ℕ → PartialIsometry M, Monotone a ∧
      (∀ n, (a n).support=q n) ∧ (∀ n, (a n).target ≤ r) := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.PartialIsometry, OAI.Generator.Tracial.PartialIsometry.target

  4. theorem OAI.Generator.Tracial.AlgebraProjection.isLUB_subequivalent_of_sequence line 86

    Source documentation

    Sequential increasing-union comparison, with a constructed compatible partial-isometry limit. No dimension-continuity premise occurs.

    theorem isLUB_subequivalent_of_sequence
    (hfactor : ∀ c : M.toStarSubalgebra,
      (∀ a : M.toStarSubalgebra, a*c=c*a) → ∃ z : ℂ, c=z • (1 : M.toStarSubalgebra))
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (q : ℕ → AlgebraProjection M) (hq : Monotone q)
    (p : AlgebraProjection M) (hp : IsLUB (Set.range q) p)
    (r : AlgebraProjection M) (hr : ∀ n, (q n).Subequivalent r) :
    p.Subequivalent r := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.AlgebraProjection.Subequivalent

  5. theorem OAI.Generator.Tracial.traceFreeDimension_range_bddAbove line 116
  6. theorem OAI.Generator.Tracial.traceFreeDimension_isLUB_sequence line 123

    Source documentation

    Continuity on sequences follows from compatible embeddings into each concrete dyadic upper approximant of the real supremum.

    theorem traceFreeDimension_isLUB_sequence
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    (q : ℕ → AlgebraProjection M) (hq : Monotone q)
    (p : AlgebraProjection M) (hp : IsLUB (Set.range q) p) :
    traceFreeDimension hfactor hdiff p =
      sSup (Set.range (fun n => traceFreeDimension hfactor hdiff (q n))) := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceFreeDimension

  7. theorem OAI.Generator.Tracial.exists_monotone_dominating_from line 150

    Source documentation

    Every countable family in a directed preorder has an increasing majorant above a specified index. This is not countable cofinality of the preorder.

    theorem exists_monotone_dominating_from
    {I : Type*} [Preorder I] [IsDirected I (· ≤ ·)] (f : ℕ → I) (i : I) :
    ∃ a : ℕ → I, Monotone a ∧ (∀ n, f n ≤ a n) ∧ (∀ n, i ≤ a n) := by
…
  8. theorem OAI.Generator.Tracial.traceFreeDimension_exists_exhausting_sequence line 168

    Source documentation

    Construct an increasing countable subfamily whose supremum dimension is the real supremum of the entire directed family. No countability is assumed.

    theorem traceFreeDimension_exists_exhausting_sequence
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    {I : Type*} [Preorder I] [IsDirected I (· ≤ ·)] [Nonempty I]
    (q : I → AlgebraProjection M) (hq : Monotone q) :
    ∃ (a : ℕ → I) (s : AlgebraProjection M), Monotone a ∧
      IsLUB (Set.range (fun n => q (a n))) s ∧
      traceFreeDimension hfactor hdiff s =
        sSup (Set.range (fun i => traceFreeDimension hfactor hdiff (q i))) := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceFreeDimension

  9. theorem OAI.Generator.Tracial.traceFreeDimension_exists_isLUB line 201

    Source documentation

    The constructed countable supremum bounds the entire net: adjoining any one index cannot increase its dimension, so strict increase forces equality.

    theorem traceFreeDimension_exists_isLUB
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    {I : Type*} [Preorder I] [IsDirected I (· ≤ ·)] [Nonempty I]
    (q : I → AlgebraProjection M) (hq : Monotone q) :
    ∃ p : AlgebraProjection M, IsLUB (Set.range q) p ∧
      traceFreeDimension hfactor hdiff p =
        sSup (Set.range (fun i => traceFreeDimension hfactor hdiff (q i))) := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceFreeDimension

  10. theorem OAI.Generator.Tracial.traceFreeDimension_isLUB_monotone line 233

    Source documentation

    Order continuity on arbitrary nonempty directed projection nets.

    theorem traceFreeDimension_isLUB_monotone
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    {I : Type*} [Preorder I] [IsDirected I (· ≤ ·)] [Nonempty I]
    (q : I → AlgebraProjection M) (hq : Monotone q)
    (p : AlgebraProjection M) (hp : IsLUB (Set.range q) p) :
    traceFreeDimension hfactor hdiff p =
      sSup (Set.range (fun i => traceFreeDimension hfactor hdiff (q i))) := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceFreeDimension

  11. theorem OAI.Generator.Tracial.traceFree_isLUB_subequivalent line 257

    Source documentation

    Arbitrary increasing-union comparison, now a consequence of the constructed dimension continuity and exact classification of comparison.

    theorem traceFree_isLUB_subequivalent
    (hfactor : ∀ c : M.toStarSubalgebra,
      (∀ a : M.toStarSubalgebra, a*c=c*a) → ∃ z : ℂ, c=z • (1 : M.toStarSubalgebra))
    (hdiff : ∀ p : M.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q : M.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p*q=q ∧ q*p=q)
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    {I : Type*} [Preorder I] [IsDirected I (· ≤ ·)] [Nonempty I]
    (q : I → AlgebraProjection M) (hq : Monotone q)
    (p : AlgebraProjection M) (hp : IsLUB (Set.range q) p)
    (r : AlgebraProjection M) (hr : ∀ i, (q i).Subequivalent r) :
    p.Subequivalent r := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection

  12. theorem OAI.Generator.isII1Factor_projection_dimension_orderContinuous line 279

    Source documentation

    The same actual dimension satisfies all finite laws and arbitrary-directed supremum continuity under exactly the original IsII1Factor hypothesis.

    theorem isII1Factor_projection_dimension_orderContinuous
    (S : StarSubalgebra ℂ (H →L[ℂ] H)) (hS : IsII1Factor S) :
    ∃ D : Tracial.AlgebraProjection (vonNeumannOfWOTClosed S hS.weaklyClosed) → ℝ,
      D ⟨1,IsStarProjection.one _⟩=1 ∧
      (∀ q, 0 ≤ D q ∧ D q ≤ 1) ∧
      (∀ q, D q=0 ↔ q.val=0) ∧
      (∀ q r, D q ≤ D r ↔ q.Subequivalent r) ∧
      (∀ q r, D q=D r ↔ q.Equivalent r) ∧
      (∀ q r (ho : q.val*r.val=0), D (Tracial.orthogonalSum q r ho)=D q+D r) ∧
      (∀ (I : Type v) [Preorder I] [IsDirected I (· ≤ ·)] [Nonempty I]
        (q : I → Tracial.AlgebraProjection (vonNeumannOfWOTClosed S hS.weaklyClosed)),
        Monotone q → ∃ p, IsLUB (Set.range q) p ∧
…

    Mentions: OAI.Generator.IsII1Factor, OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.vonNeumannOfWOTClosed, OAI.Generator.Tracial.orthogonalSum

  13. theorem OAI.Generator.Tracial.traceFreeDimension_exists_small_subprojection line 335
  14. theorem OAI.Generator.Tracial.traceFreeDimension_bounded_chain line 364
  15. theorem OAI.Generator.Tracial.traceFreeDimension_exists_maximal_below line 385
  16. theorem OAI.Generator.Tracial.traceFreeDimension_exists_subprojection line 408

    Source documentation

    Every dimension between zero and D(p) is realized inside p.

    theorem traceFreeDimension_exists_subprojection
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    (p : AlgebraProjection M) (d : ℝ) (hd : 0 ≤ d)
    (hdp : d ≤ traceFreeDimension hfactor hdiff p) :
    ∃ q : AlgebraProjection M, q ≤ p ∧ traceFreeDimension hfactor hdiff q=d := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceFreeDimension

  17. theorem OAI.Generator.Tracial.traceFreeDimension_remainder line 455
  18. theorem OAI.Generator.Tracial.traceFreeDimension_exists_partition line 472

    Source documentation

    Every prescribed finite list of nonnegative dimensions summing to D(p) is realized by pairwise orthogonal actual projections summing to p.

    theorem traceFreeDimension_exists_partition
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    (n : ℕ) (p : AlgebraProjection M) (d : Fin n → ℝ)
    (hd : ∀ i, 0 ≤ d i) (hsum : ∑ i, d i=traceFreeDimension hfactor hdiff p) :
    ∃ q : Fin n → AlgebraProjection M, (∀ i, q i ≤ p) ∧
      (∀ i j, i≠j → (q i).val*(q j).val=0) ∧
      (∑ i, (q i).val)=p.val ∧ (∀ i, traceFreeDimension hfactor hdiff (q i)=d i) := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceFreeDimension

  19. theorem OAI.Generator.Tracial.traceFreeDimension_exists_uniform_partition line 528

    Source documentation

    A finite corner partition into n equal dimensions, for every n>0.

    theorem traceFreeDimension_exists_uniform_partition
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    (n : ℕ) (hn : 0<n) (p : AlgebraProjection M) :
    ∃ q : Fin n → AlgebraProjection M, (∀ i, q i ≤ p) ∧
      (∀ i j, i≠j → (q i).val*(q j).val=0) ∧
      (∑ i, (q i).val)=p.val ∧
      (∀ i, traceFreeDimension hfactor hdiff (q i)=traceFreeDimension hfactor hdiff p/n) := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceFreeDimension

  20. theorem OAI.Generator.Tracial.traceFreeDimension_exists_equivalent_partition line 544

    Source documentation

    Actual matrix-unit legs for a partition of every positive finite size.

    theorem traceFreeDimension_exists_equivalent_partition
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    (n : ℕ) (hn : 0<n) (p : AlgebraProjection M) :
    Nonempty (EquivalentPartition p (Fin n)) := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.EquivalentPartition

  21. def OAI.Generator.Tracial.AlgebraProjection.vectorValue line 578

    Source documentation

    The original Hilbert-space vector functional on actual projections.

    def vectorValue (ξ : H) (p : AlgebraProjection M) : ℝ :=
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection

  22. theorem OAI.Generator.Tracial.AlgebraProjection.vectorValue_eq_norm_sq line 581
  23. theorem OAI.Generator.Tracial.AlgebraProjection.vectorValue_nonneg line 592
  24. theorem OAI.Generator.Tracial.AlgebraProjection.vectorValue_remainder line 596
  25. theorem OAI.Generator.Tracial.AlgebraProjection.vectorValue_mono line 602
  26. theorem OAI.Generator.Tracial.AlgebraProjection.exists_isLUB_monotone_vector_limit line 610

    Source documentation

    Retains the matrix-coefficient limit of the concrete projection supremum. The ultrafilter is the fixed extension of atTop, not a countable subsequence.

    theorem exists_isLUB_monotone_vector_limit
    {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (a : ι → AlgebraProjection M) (ha : Monotone a) :
    ∃ p : AlgebraProjection M, IsLUB (Set.range a) p ∧
      ∀ x y : H, Tendsto (fun i => inner ℂ y ((a i).val.val x))
        ((Ultrafilter.of atTop : Ultrafilter ι) : Filter ι) (𝓝 (inner ℂ y (p.val.val x))) := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection

  27. theorem OAI.Generator.Tracial.AlgebraProjection.vectorValue_isLUB_monotone line 679

    Source documentation

    The vector functional preserves any directed projection supremum.

    theorem vectorValue_isLUB_monotone
    {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (a : ι → AlgebraProjection M) (ha : Monotone a)
    (p : AlgebraProjection M) (hp : IsLUB (Set.range a) p) (ξ : H) :
    IsLUB (Set.range (fun i => vectorValue ξ (a i))) (vectorValue ξ p) := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.AlgebraProjection.vectorValue

  28. theorem OAI.Generator.Tracial.AlgebraProjection.vectorValue_tendsto_monotone line 694