OAI/Analysis/FactorGeneration/Dimension.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Archimedean comparison for the constructed dyadic reference projections. Orthogonal sibling corners supply copies for the finite-algebra shift argument.

  1. def OAI.Generator.Tracial.dyadicFalseIndex line 18

    Source documentation

    Follow the false child at every level of the actual coherent dyadic system.

    def dyadicFalseIndex : (n : ℕ) → DyadicIndex n
  | 0 => ()
  | n+1 => (dyadicFalseIndex n,false)

variable (hfactor : ∀ c : M.toStarSubalgebra,
  (∀ a : M.toStarSubalgebra, a*c=c*a) → ∃ z : ℂ, c=z • (1 : M.toStarSubalgebra))
variable (hdiff : ∀ p : M.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
  ∃ q : M.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p*q=q ∧ q*p=q)

    Mentions: OAI.Generator.Tracial.DyadicIndex

  2. def OAI.Generator.Tracial.traceFreeDyadicReference line 27
  3. def OAI.Generator.Tracial.traceFreeDyadicSibling line 30
  4. theorem OAI.Generator.Tracial.traceFreeDyadicReference_zero line 33
  5. theorem OAI.Generator.Tracial.traceFreeDyadic_child_le line 37
  6. theorem OAI.Generator.Tracial.traceFreeDyadicReference_antitone line 45
  7. theorem OAI.Generator.Tracial.traceFreeDyadicSibling_le line 51
  8. theorem OAI.Generator.Tracial.traceFreeDyadicReference_sibling_orthogonal line 55
  9. theorem OAI.Generator.Tracial.traceFreeDyadicSibling_orthogonal line 61
  10. theorem OAI.Generator.Tracial.traceFreeDyadicReference_equivalent_sibling line 76
  11. theorem OAI.Generator.Tracial.traceFreeDyadicReference_ne_zero line 83
  12. theorem OAI.Generator.Tracial.traceFree_dyadic_archimedean line 89

    Source documentation

    A projection that embeds in every dyadic reference corner must be zero. Finiteness is used through the constructed infinite shift, not through a trace.

    theorem traceFree_dyadic_archimedean
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (p r : AlgebraProjection M)
    (h : ∀ n, r.Subequivalent (traceFreeDyadicReference hfactor hdiff p n)) : r.val=0 := by
…

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

  13. theorem OAI.Generator.Tracial.traceFree_dyadic_archimedean_witnesses line 101

    Source documentation

    Archimedean comparison with explicit partial-isometry witnesses.

    theorem traceFree_dyadic_archimedean_witnesses
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (p r : AlgebraProjection M)
    (h : ∀ n, ∃ v : PartialIsometry M, v.support=r ∧
      v.target ≤ traceFreeDyadicReference hfactor hdiff p n) : r.val=0 :=
…

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

  14. theorem OAI.Generator.Tracial.traceFree_exists_dyadic_obstruction line 109

    Source documentation

    Every nonzero projection eventually fails to fit into the dyadic corners.

    theorem traceFree_exists_dyadic_obstruction
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (p r : AlgebraProjection M) (hr : r.val≠0) :
    ∃ n, ¬r.Subequivalent (traceFreeDyadicReference hfactor hdiff p n) := by
…

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

  15. theorem OAI.Generator.Tracial.traceFree_eventually_dyadic_subequivalent line 119

    Source documentation

    Every nonzero projection contains an equivalent copy of every sufficiently small dyadic reference piece. This supplies the positivity input for dimension.

    theorem traceFree_eventually_dyadic_subequivalent
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (p r : AlgebraProjection M) (hr : r.val≠0) :
    ∃ n, ∀ m, n ≤ m → (traceFreeDyadicReference hfactor hdiff p m).Subequivalent r := by
…

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

  16. theorem OAI.Generator.isII1Factor_archimedean_reference line 136

    Source documentation

    The unchanged original finite diffuse factor has a decreasing sequence of nonzero dyadic reference projections satisfying Archimedean comparison.

    theorem isII1Factor_archimedean_reference
    (S : StarSubalgebra ℂ (H →L[ℂ] H)) (hS : IsII1Factor S) :
    ∃ e : ℕ → Tracial.AlgebraProjection (vonNeumannOfWOTClosed S hS.weaklyClosed),
      (e 0).val=1 ∧ Antitone e ∧ (∀ n, (e n).val≠0) ∧
      ∀ r : Tracial.AlgebraProjection (vonNeumannOfWOTClosed S hS.weaklyClosed),
        (∀ n, r.Subequivalent (e n)) → r.val=0 := by
…

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

  17. theorem OAI.Generator.Tracial.EquivalentPartition.exists_maximal_fitting_subset line 172
  18. theorem OAI.Generator.Tracial.EquivalentPartition.maximal_remainder_not_subequivalent line 186

    Source documentation

    A further piece in the remainder would enlarge the fitting subset.

    theorem maximal_remainder_not_subequivalent (E : EquivalentPartition p ι)
    (q : AlgebraProjection M) (s : Finset ι)
    (hmax : ∀ t : Finset ι, (E.subset t).Subequivalent q → t.card ≤ s.card)
    (v : PartialIsometry M) (hv : v.support=E.subset s) (ht : v.target ≤ q)
    (i : ι) (hi : i ∉ s) :
    ¬(E.leg i).target.Subequivalent (AlgebraProjection.remainder v.target q ht) := by
…

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

  19. theorem OAI.Generator.Tracial.EquivalentPartition.exists_subset_rounding line 217

    Source documentation

    Every projection inside the partition unit lies between subset sums whose cardinalities differ by at most one. This is operator comparison, not a trace estimate and not an assumed dimension rounding law.

    theorem exists_subset_rounding
    (hfactor : ∀ c : M.toStarSubalgebra,
      (∀ a : M.toStarSubalgebra, a*c=c*a) → ∃ z : ℂ, c=z • (1 : M.toStarSubalgebra))
    (E : EquivalentPartition p ι) (q : AlgebraProjection M) (hqp : q ≤ p) :
    ∃ s t : Finset ι, s ⊆ t ∧ t.card ≤ s.card+1 ∧
      (E.subset s).Subequivalent q ∧ q.Subequivalent (E.subset t) ∧
      ∀ a : Finset ι, (E.subset a).Subequivalent q → a.card ≤ s.card := by
…

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

  20. def OAI.Generator.Tracial.dyadicWeight line 256
  21. theorem OAI.Generator.Tracial.dyadicWeight_nonneg line 258
  22. theorem OAI.Generator.Tracial.dyadicWeight_le_one line 261
  23. theorem OAI.Generator.Tracial.dyadicWeight_univ line 266
  24. theorem OAI.Generator.Tracial.dyadicWeight_children line 271
  25. def OAI.Generator.Tracial.traceFreeDyadicCut line 283

    Source documentation

    Membership contains an actual partial-isometry witness through Subequivalent.

    def traceFreeDyadicCut (p q : AlgebraProjection M) : Set ℝ :=
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection

  26. def OAI.Generator.Tracial.traceFreeDyadicSup line 288
  27. theorem OAI.Generator.Tracial.traceFreeDyadicCut_zero_mem line 291
  28. theorem OAI.Generator.Tracial.traceFreeDyadicCut_bddAbove line 298
  29. theorem OAI.Generator.Tracial.traceFreeDyadicSup_nonneg line 304
  30. theorem OAI.Generator.Tracial.traceFreeDyadicSup_le_one line 309
  31. theorem OAI.Generator.Tracial.traceFreeDyadicSup_lower_bound line 315
  32. theorem OAI.Generator.Tracial.traceFreeDyadicCut_mono line 321
  33. theorem OAI.Generator.Tracial.traceFreeDyadicSup_mono line 327
  34. theorem OAI.Generator.Tracial.traceFreeDyadicSup_equivalent line 334
  35. theorem OAI.Generator.Tracial.traceFreeDyadicSup_self line 340
  36. theorem OAI.Generator.Tracial.traceFreeDyadicCut_refine line 349

    Source documentation

    Refining to all children preserves both the actual projection and weight.

    theorem traceFreeDyadicCut_refine (p q : AlgebraProjection M) (n : ℕ)
    (s : Finset (DyadicIndex n))
    (h : ((traceFreeDyadicPartition hfactor hdiff p n).subset s).Subequivalent q) :
    ((traceFreeDyadicPartition hfactor hdiff p (n+1)).subset
      (s ×ˢ (Finset.univ : Finset Bool))).Subequivalent q ∧
      dyadicWeight (n+1) (s ×ˢ (Finset.univ : Finset Bool))=dyadicWeight n s := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.DyadicIndex, OAI.Generator.Tracial.traceFreeDyadicPartition, OAI.Generator.Tracial.dyadicWeight

  37. theorem OAI.Generator.Tracial.traceFreeDyadicSup_zero line 360
  38. theorem OAI.Generator.Tracial.traceFreeDyadicSup_pos line 384

    Source documentation

    Archimedean comparison makes the supremum strictly positive on nonzero projections.

    theorem traceFreeDyadicSup_pos
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (p q : AlgebraProjection M) (hq : q.val≠0) :
    0 < traceFreeDyadicSup hfactor hdiff p q := by
…

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

  39. theorem OAI.Generator.Tracial.traceFreeDyadicSup_eq_zero_iff line 397
  40. theorem OAI.Generator.Tracial.dyadicWeight_le_iff line 418
  41. theorem OAI.Generator.Tracial.traceFreeDyadic_exists_refined_subset line 429
  42. theorem OAI.Generator.Tracial.traceFreeDyadic_comparison_iff_weight line 444

    Source documentation

    Comparison between any two levels agrees with the real dyadic weights.

    theorem traceFreeDyadic_comparison_iff_weight
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (p : AlgebraProjection M) (hp : p.val≠0) (n m : ℕ)
    (s : Finset (DyadicIndex n)) (t : Finset (DyadicIndex m)) :
    ((traceFreeDyadicPartition hfactor hdiff p n).subset s).Subequivalent
      ((traceFreeDyadicPartition hfactor hdiff p m).subset t) ↔
        dyadicWeight n s ≤ dyadicWeight m t := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.DyadicIndex, OAI.Generator.Tracial.traceFreeDyadicPartition, OAI.Generator.Tracial.dyadicWeight

  43. theorem OAI.Generator.Tracial.traceFreeDyadicSup_subset line 458
  44. theorem OAI.Generator.Tracial.traceFreeDyadicSup_rounding line 471

    Source documentation

    At every level the cut supremum has actual lower and upper operator witnesses, with a numerical gap at most 2^(-n).

    theorem traceFreeDyadicSup_rounding
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (p q : AlgebraProjection M) (hp : p.val≠0) (hq : q ≤ p) (n : ℕ) :
    ∃ s t : Finset (DyadicIndex n), s ⊆ t ∧ t.card ≤ s.card+1 ∧
      ((traceFreeDyadicPartition hfactor hdiff p n).subset s).Subequivalent q ∧
      q.Subequivalent ((traceFreeDyadicPartition hfactor hdiff p n).subset t) ∧
      dyadicWeight n s ≤ traceFreeDyadicSup hfactor hdiff p q ∧
      traceFreeDyadicSup hfactor hdiff p q ≤ dyadicWeight n t ∧
      dyadicWeight n t ≤ dyadicWeight n s+1/2^n := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.DyadicIndex, OAI.Generator.Tracial.traceFreeDyadicPartition, OAI.Generator.Tracial.dyadicWeight, OAI.Generator.Tracial.traceFreeDyadicSup

  45. theorem OAI.Generator.Tracial.EquivalentPartition.subset_complement line 501
  46. theorem OAI.Generator.Tracial.EquivalentPartition.exists_disjoint_card line 509
  47. theorem OAI.Generator.Tracial.EquivalentPartition.orthogonal_fitting_card_bound line 521

    Source documentation

    Two orthogonal fitting projections cannot use more pieces than the unit.

    theorem orthogonal_fitting_card_bound
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (hfactor : ∀ c : M.toStarSubalgebra,
      (∀ a : M.toStarSubalgebra, a*c=c*a) → ∃ z : ℂ, c=z • (1 : M.toStarSubalgebra))
    (E : EquivalentPartition p ι) (hp : p.val≠0)
    (q r : AlgebraProjection M) (hqp : q ≤ p) (hrp : r ≤ p) (ho : q.val*r.val=0)
    (s t : Finset ι) (hs : (E.subset s).Subequivalent q) (ht : (E.subset t).Subequivalent r) :
    s.card+t.card ≤ Fintype.card ι := by
…

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

  48. theorem OAI.Generator.Tracial.EquivalentPartition.orthogonal_fitting_union line 549

    Source documentation

    Disjoint replacement of one collection lets the actual witnesses be added.

    theorem orthogonal_fitting_union
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (hfactor : ∀ c : M.toStarSubalgebra,
      (∀ a : M.toStarSubalgebra, a*c=c*a) → ∃ z : ℂ, c=z • (1 : M.toStarSubalgebra))
    (E : EquivalentPartition p ι) (hp : p.val≠0)
    (q r : AlgebraProjection M) (hqp : q ≤ p) (hrp : r ≤ p) (ho : q.val*r.val=0)
    (s t : Finset ι) (hs : (E.subset s).Subequivalent q) (ht : (E.subset t).Subequivalent r) :
    ∃ u : Finset ι, u.card=s.card+t.card ∧
      (E.subset u).Subequivalent (orthogonalSum q r ho) := by
…

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

  49. theorem OAI.Generator.Tracial.EquivalentPartition.orthogonal_upper_union line 568
  50. theorem OAI.Generator.Tracial.eq_of_all_dyadic_errors line 592
  51. theorem OAI.Generator.Tracial.traceFreeDyadicSup_lower_add line 608
  52. theorem OAI.Generator.Tracial.traceFreeDyadicSup_upper_add line 621
  53. theorem OAI.Generator.Tracial.traceFreeDyadicSup_orthogonal_add line 644

    Source documentation

    The dyadic supremum is additive on actual orthogonal projections below p.

    theorem traceFreeDyadicSup_orthogonal_add
    (p q r : AlgebraProjection M) (hp : p.val≠0) (hqp : q ≤ p) (hrp : r ≤ p)
    (ho : q.val*r.val=0) :
    traceFreeDyadicSup hfactor hdiff p (orthogonalSum q r ho)=
      traceFreeDyadicSup hfactor hdiff p q+traceFreeDyadicSup hfactor hdiff p r := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceFreeDyadicSup, OAI.Generator.Tracial.orthogonalSum

  54. theorem OAI.Generator.Tracial.traceFreeDyadicSup_remainder line 662
  55. theorem OAI.Generator.Tracial.traceFreeDyadicSup_strictMono line 674

    Source documentation

    Faithfulness and additivity give strict increase along proper inclusion.

    theorem traceFreeDyadicSup_strictMono
    (p q r : AlgebraProjection M) (hp : p.val≠0) (hrp : r ≤ p) (hqr : q < r) :
    traceFreeDyadicSup hfactor hdiff p q < traceFreeDyadicSup hfactor hdiff p r := by
…

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

  56. theorem OAI.Generator.Tracial.traceFree_target_eq_of_dimension_le line 706
  57. theorem OAI.Generator.Tracial.traceFreeDyadicSup_le_iff_subequivalent line 720

    Source documentation

    Real-valued comparison is exactly witnessed projection subequivalence.

    theorem traceFreeDyadicSup_le_iff_subequivalent
    (p q r : AlgebraProjection M) (hp : p.val≠0) (hqp : q ≤ p) :
    traceFreeDyadicSup hfactor hdiff p q ≤ traceFreeDyadicSup hfactor hdiff p r ↔
      q.Subequivalent r := by
…

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

  58. theorem OAI.Generator.Tracial.traceFreeDyadicSup_eq_iff_equivalent line 733
  59. def OAI.Generator.Tracial.traceFreeDimension line 745

    Source documentation

    The same constructed lower cut, now normalized at the algebra identity.

    def traceFreeDimension (q : AlgebraProjection M) : ℝ :=
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection

  60. theorem OAI.Generator.isII1Factor_projection_dimension line 753

    Source documentation

    The original nonzero finite diffuse factor has a normalized faithful finitely additive dimension on its actual projections. The comparison equivalences use actual partial isometries, not a supplied dimension oracle.

    theorem isII1Factor_projection_dimension
    (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) := by
…

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

  61. theorem OAI.Generator.Tracial.traceFreeDimension_nonneg line 802
  62. theorem OAI.Generator.Tracial.traceFreeDimension_le_one line 806
  63. theorem OAI.Generator.Tracial.traceFreeDimension_subequivalent line 810
  64. theorem OAI.Generator.Tracial.traceFreeDimension_mono line 815
  65. theorem OAI.Generator.Tracial.traceFreeDimension_le_iff_subequivalent line 820
  66. theorem OAI.Generator.Tracial.traceFreeDimension_strictMono line 827
  67. theorem OAI.Generator.Tracial.exists_dyadicWeight_upper line 832

    Source documentation

    A subset of the n-th reference partition with weight in [c,c+2^(-n)].

    theorem exists_dyadicWeight_upper (c : ℝ) (hc : 0 ≤ c) (hc1 : c ≤ 1) (n : ℕ) :
    ∃ s : Finset (DyadicIndex n), c ≤ dyadicWeight n s ∧ dyadicWeight n s ≤ c+1/2^n := by
…

    Mentions: OAI.Generator.Tracial.DyadicIndex, OAI.Generator.Tracial.dyadicWeight

  68. theorem OAI.Generator.Tracial.traceFreeDimension_exists_upper line 855

    Source documentation

    Actual projection upper approximants for every real c in [0,1].

    theorem traceFreeDimension_exists_upper
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    (c : ℝ) (hc : 0 ≤ c) (hc1 : c ≤ 1) (n : ℕ) :
    ∃ r : AlgebraProjection M, c ≤ traceFreeDimension hfactor hdiff r ∧
      traceFreeDimension hfactor hdiff r ≤ c+1/2^n := by
…

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

  69. theorem OAI.Generator.Tracial.le_of_all_dyadic_errors line 867