DyadicComparison.lean`

94 declarations, 0 contain sorry, 0 declared as axioms

Halving every projection in a diffuse factor without a trace. Maximality leaves no residual corner: a diffuse residual splits into two nonzero orthogonal projections, and a polar link gives a strict extension.

def OAI.Generator.Tracial.orthogonalSum line 20
Source documentation
The sum of two orthogonal projections, in the original algebra.
```
def orthogonalSum (p q : AlgebraProjection M) (h : p.val*q.val=0) : AlgebraProjection M :=
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.le_orthogonalSum_left line 23
theorem OAI.Generator.Tracial.le_orthogonalSum_right line 28
theorem OAI.Generator.Tracial.orthogonalSum_le line 33

theorem OAI.Generator.Tracial.traceFree_exists_orthogonal_split line 39

Source documentation

A proper diffuse subprojection splits a nonzero corner into orthogonal pieces.

theorem traceFree_exists_orthogonal_split
    (hdiff : ∀ p : M.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q : M.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p*q=q ∧ q*p=q)
    (p : AlgebraProjection M) (hp : p.val≠0) :
    ∃ q r : AlgebraProjection M, q ≤ p ∧ r ≤ p ∧ q.val≠0 ∧ r.val≠0 ∧
      q.val*r.val=0 ∧ q.val+r.val=p.val := by
…

Mentions: OAI.Generator.Tracial.AlgebraProjection

theorem OAI.Generator.Tracial.traceFree_exists_halving line 57

Source documentation

The two equivalent halves are constructed by an actual partial isometry. No trace, finite-isometry property, or separability is needed for this lemma.

theorem traceFree_exists_halving
    (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)
    (p : AlgebraProjection M) :
    ∃ v : PartialIsometry M, v.support.val*v.target.val=0 ∧
      v.support.val+v.target.val=p.val := by
…

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

theorem OAI.Generator.isII1Factor_halving line 108
Source documentation
Halving in exactly the original concrete factor; the bicommutant packaging does not change its operators, projection predicates, or algebra operations.
```
theorem isII1Factor_halving
    (S : StarSubalgebra ℂ (H →L[ℂ] H)) (hS : IsII1Factor S)
    (p : Tracial.AlgebraProjection (vonNeumannOfWOTClosed S hS.weaklyClosed)) :
    ∃ v : Tracial.PartialIsometry (vonNeumannOfWOTClosed S hS.weaklyClosed),
      v.support.val*v.target.val=0 ∧ v.support.val+v.target.val=p.val := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.vonNeumannOfWOTClosed, OAI.Generator.Tracial.PartialIsometry
def OAI.Generator.Tracial.PartialIsometry.compose line 131
Source documentation
Composition with range contained in the initial projection.
```
def compose (v w : PartialIsometry M) (h : w.target ≤ v.support) : PartialIsometry M where
…
```
Mentions: OAI.Generator.Tracial.PartialIsometry
theorem OAI.Generator.Tracial.PartialIsometry.compose_target line 141
theorem OAI.Generator.Tracial.PartialIsometry.compose_target_le line 146
structure OAI.Generator.Tracial.EquivalentPartition line 156
Source documentation
A partition of p with actual partial isometries from a common projection. The cross identities encode orthogonality. This structure is constructed below.
```
structure EquivalentPartition (p : AlgebraProjection M) (ι : Type*) [Fintype ι] where
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.EquivalentPartition.orthogonal line 167
def OAI.Generator.Tracial.EquivalentPartition.link line 175
Source documentation
Every ordered pair of pieces has a displayed equivalence witness.
```
def link (E : EquivalentPartition p ι) (i j : ι) : PartialIsometry M :=
…
```
Mentions: OAI.Generator.Tracial.EquivalentPartition, OAI.Generator.Tracial.PartialIsometry
theorem OAI.Generator.Tracial.EquivalentPartition.link_support line 183
theorem OAI.Generator.Tracial.EquivalentPartition.link_target line 186
def OAI.Generator.Tracial.EquivalentPartition.refine line 197
Source documentation
Refinement is performed on the common initial corner and transported.
```
def refine (E : EquivalentPartition p ι) (F : EquivalentPartition E.base κ) :
    EquivalentPartition p (ι × κ) where
…
```
Mentions: OAI.Generator.Tracial.EquivalentPartition
theorem OAI.Generator.Tracial.EquivalentPartition.refine_parent line 225
def OAI.Generator.Tracial.EquivalentPartition.singleton line 233
Source documentation
Depth zero consists of the original projection itself.
```
def singleton (p : AlgebraProjection M) : EquivalentPartition p Unit where
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.EquivalentPartition
def OAI.Generator.Tracial.EquivalentPartition.ofHalving line 242
Source documentation
Two equivalent orthogonal halves, as a family with a common initial corner.
```
def ofHalving (v : PartialIsometry M) (ho : v.support.val*v.target.val=0)
    (hp : v.support.val+v.target.val=p.val) : EquivalentPartition p Bool where
…
```
Mentions: OAI.Generator.Tracial.PartialIsometry, OAI.Generator.Tracial.EquivalentPartition
def OAI.Generator.Tracial.EquivalentPartition.entry line 283
Source documentation
The matrix entries associated to the explicit common-source legs.
```
def entry (E : EquivalentPartition p ι) (i j : ι) : M.toStarSubalgebra :=
…
```
Mentions: OAI.Generator.Tracial.EquivalentPartition
theorem OAI.Generator.Tracial.EquivalentPartition.entry_diagonal line 286
theorem OAI.Generator.Tracial.EquivalentPartition.entry_star line 289
theorem OAI.Generator.Tracial.EquivalentPartition.entry_mul line 292
theorem OAI.Generator.Tracial.EquivalentPartition.refine_entry line 306
Source documentation
Every old matrix entry is exactly the sum of its corresponding child entries.
```
theorem refine_entry (E : EquivalentPartition p ι) (F : EquivalentPartition E.base κ)
    (i j : ι) : (∑ b, (E.refine F).entry (i,b) (j,b))=E.entry i j := by
…
```
Mentions: OAI.Generator.Tracial.EquivalentPartition, OAI.Generator.Tracial.EquivalentPartition.entry
def OAI.Generator.Tracial.EquivalentPartition.matrixUnits line 318
Source documentation
A partition of the identity yields a unital full matrix-unit system.
```
def matrixUnits [DecidableEq ι] (E : EquivalentPartition p ι) (hp : p.val=1) :
    MatrixUnitSystem ι M.toStarSubalgebra where
…
```
Mentions: OAI.Generator.Tracial.EquivalentPartition, OAI.Generator.MatrixUnitSystem
theorem OAI.Generator.Tracial.EquivalentPartition.target_ne_zero line 327
Source documentation
A partition of a nonzero projection has no zero piece, since every piece is equivalent to every other piece by the displayed links.
```
theorem target_ne_zero (E : EquivalentPartition p ι) (hp : p.val≠0) (i : ι) :
    (E.leg i).target.val≠0 := by
…
```
Mentions: OAI.Generator.Tracial.EquivalentPartition
def OAI.Generator.Tracial.traceFreeBinaryPartition line 350
Source documentation
Choose the actual two-leg partition supplied by trace-free halving.
```
def traceFreeBinaryPartition (p : AlgebraProjection M) : EquivalentPartition p Bool :=
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.EquivalentPartition
def OAI.Generator.Tracial.traceFreeDyadicPartition line 356
Source documentation
A coherent family: each successor halves the previous common initial projection once and transports that halving to all its equivalent pieces.
```
def traceFreeDyadicPartition (p : AlgebraProjection M) :
    (n : ℕ) → EquivalentPartition p (DyadicIndex n)
  | 0 => EquivalentPartition.singleton p
  | n+1 =>
    let E := traceFreeDyadicPartition p n
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.EquivalentPartition, OAI.Generator.Tracial.DyadicIndex, OAI.Generator.Tracial.EquivalentPartition.singleton
theorem OAI.Generator.Tracial.traceFreeDyadicPartition_parent line 363
theorem OAI.Generator.Tracial.traceFreeDyadicPartition_entry line 368
def OAI.Generator.Tracial.traceFreeDyadicMatrixUnits line 375
Source documentation
Actual matrix units of sizes 2^n, with coherent inclusions.
```
def traceFreeDyadicMatrixUnits (n : ℕ) : MatrixUnitSystem (DyadicIndex n) M.toStarSubalgebra :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.Generator.Tracial.DyadicIndex
theorem OAI.Generator.Tracial.traceFreeDyadicMatrixUnits_compatible line 378

theorem OAI.Generator.isII1Factor_dyadic_matrixUnits line 386

Source documentation

Coherent dyadic matrix units in the unchanged original concrete factor.

theorem isII1Factor_dyadic_matrixUnits
    (S : StarSubalgebra ℂ (H →L[ℂ] H)) (hS : IsII1Factor S) :
    ∃ E : (n : ℕ) → MatrixUnitSystem (Tracial.DyadicIndex n) S,
      ∀ (n : ℕ) (i j : Tracial.DyadicIndex n),
        (∑ b : Bool, (E (n+1)).entry (i,b) (j,b))=(E n).entry i j := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.Generator.MatrixUnitSystem, OAI.Generator.Tracial.DyadicIndex

theorem OAI.Generator.Tracial.PartialIsometry.exists_orthogonalPartialSum line 417
def OAI.Generator.Tracial.PartialIsometry.orthogonalPartialSum line 438
theorem OAI.Generator.Tracial.PartialIsometry.orthogonalPartialSum_val line 441
theorem OAI.Generator.Tracial.PartialIsometry.orthogonalPartialSum_support line 445
theorem OAI.Generator.Tracial.PartialIsometry.orthogonalPartialSum_target line 449
theorem OAI.Generator.Tracial.PartialIsometry.le_orthogonalPartialSum line 453
theorem OAI.Generator.Tracial.PartialIsometry.orthogonalPartialSum_monotone line 463
theorem OAI.Generator.Tracial.PartialIsometry.traceFree_orthogonal_sum line 484
Source documentation
An actual infinite orthogonal sum, with least upper bound characterizations for both support projections. It may be used to construct a shift.
```
theorem traceFree_orthogonal_sum :
    ∃ v : PartialIsometry M, (∀ i, a i ≤ v) ∧
      (∀ p : AlgebraProjection M, v.support ≤ p ↔ ∀ i, (a i).support ≤ p) ∧
      (∀ q : AlgebraProjection M, v.target ≤ q ↔ ∀ i, (a i).target ≤ q) := by
…
```
Mentions: OAI.Generator.Tracial.PartialIsometry, OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.PartialIsometry.target
theorem OAI.Generator.Tracial.PartialIsometry.adjoint_target line 515
theorem OAI.Generator.Tracial.PartialIsometry.compose_target_of_eq line 520
def OAI.Generator.Tracial.PartialIsometry.rangeLink line 527
Source documentation
Link two ranges whose displayed partial isometries have the same source.
```
def rangeLink (v w : PartialIsometry M) (h : v.support=w.support) : PartialIsometry M :=
…
```
Mentions: OAI.Generator.Tracial.PartialIsometry
theorem OAI.Generator.Tracial.PartialIsometry.rangeLink_support line 530
theorem OAI.Generator.Tracial.PartialIsometry.rangeLink_target line 533
def OAI.Generator.Tracial.AlgebraProjection.Subequivalent line 540
def OAI.Generator.Tracial.AlgebraProjection.Equivalent line 543
theorem OAI.Generator.Tracial.AlgebraProjection.subequivalent_refl line 546
theorem OAI.Generator.Tracial.AlgebraProjection.subequivalent_of_le line 549
theorem OAI.Generator.Tracial.AlgebraProjection.subequivalent_trans line 553
theorem OAI.Generator.Tracial.AlgebraProjection.equivalent_refl line 560
theorem OAI.Generator.Tracial.AlgebraProjection.equivalent_symm line 563
theorem OAI.Generator.Tracial.AlgebraProjection.equivalent_trans line 567
theorem OAI.Generator.Tracial.AlgebraProjection.Equivalent.subequivalent line 574

theorem OAI.Generator.Tracial.AlgebraProjection.subequivalent_total line 580

Source documentation

Scalar-center comparison gives totality of actual subequivalence.

theorem subequivalent_total
    (hfactor : ∀ c : M.toStarSubalgebra,
      (∀ a : M.toStarSubalgebra, a*c=c*a) → ∃ z : ℂ, c=z • (1 : M.toStarSubalgebra))
    (p q : AlgebraProjection M) : p.Subequivalent q ∨ q.Subequivalent p := by
…

Mentions: OAI.Generator.Tracial.AlgebraProjection

theorem OAI.Generator.Tracial.traceFree_finite_orthogonal_copies_eq_zero line 596
Source documentation
The infinite shift omits the first range. Finiteness then forces that range, and hence the common source projection, to be zero.
```
theorem traceFree_finite_orthogonal_copies_eq_zero
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (r : AlgebraProjection M) (a : ℕ → PartialIsometry M)
    (hs : ∀ i, (a i).support=r)
    (ho : ∀ i j, i≠j → (a i).target.val*(a j).target.val=0) : r.val=0 := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.PartialIsometry

theorem OAI.Generator.Tracial.traceFree_finite_subequivalent_orthogonal_eq_zero line 636

Source documentation

Subequivalence into every member of an orthogonal sequence is impossible for a nonzero projection in a finite algebra.

theorem traceFree_finite_subequivalent_orthogonal_eq_zero
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (r : AlgebraProjection M) (q : ℕ → AlgebraProjection M)
    (ho : ∀ i j, i≠j → (q i).val*(q j).val=0)
    (h : ∀ i, r.Subequivalent (q i)) : r.val=0 := by
…

Mentions: OAI.Generator.Tracial.AlgebraProjection

theorem OAI.Generator.Tracial.AlgebraProjection.equivalent_of_mutual_subequivalent line 654
Source documentation
Mutual subequivalence is equivalence in a finite algebra.
```
theorem equivalent_of_mutual_subequivalent {p q : AlgebraProjection M}
    (hpq : p.Subequivalent q) (hqp : q.Subequivalent p) : p.Equivalent q := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.AlgebraProjection.eq_of_equivalent_of_le line 671
Source documentation
Equivalent comparable projections in a finite algebra coincide.
```
theorem eq_of_equivalent_of_le {p q : AlgebraProjection M}
    (he : p.Equivalent q) (hle : p ≤ q) : p=q := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.AlgebraProjection.target_eq_of_equivalent line 679
Source documentation
Any embedding onto a subprojection of an equivalent projection is onto.
```
theorem target_eq_of_equivalent (v : PartialIsometry M) (q : AlgebraProjection M)
    (he : v.support.Equivalent q) (hle : v.target ≤ q) : v.target=q := by
…
```
Mentions: OAI.Generator.Tracial.PartialIsometry, OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.AlgebraProjection.subequivalent_orthogonalSum line 684
theorem OAI.Generator.Tracial.AlgebraProjection.equivalent_orthogonalSum line 702
theorem OAI.Generator.Tracial.AlgebraProjection.subequivalent_cancel line 722
Source documentation
Cancel equivalent orthogonal pieces from a subequivalence.
```
theorem subequivalent_cancel {p q r s : AlgebraProjection M}
    (hp : p.val*r.val=0) (hq : q.val*s.val=0) (he : p.Equivalent q)
    (h : (orthogonalSum p r hp).Subequivalent (orthogonalSum q s hq)) :
    r.Subequivalent s := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.orthogonalSum, OAI.Generator.Tracial.AlgebraProjection.Subequivalent
theorem OAI.Generator.Tracial.AlgebraProjection.equivalent_cancel line 752
def OAI.Generator.Tracial.AlgebraProjection.remainder line 762
Source documentation
The relative complement is the actual difference of the operators.
```
def remainder (p q : AlgebraProjection M) (h : p ≤ q) : AlgebraProjection M :=
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.AlgebraProjection.remainder_orthogonal line 765
theorem OAI.Generator.Tracial.AlgebraProjection.orthogonalSum_remainder line 770
theorem OAI.Generator.Tracial.AlgebraProjection.remainder_le line 774
theorem OAI.Generator.Tracial.AlgebraProjection.remainder_subequivalent line 780
Source documentation
Comparison respects subtraction of equivalent pieces.
```
theorem remainder_subequivalent {p q P Q : AlgebraProjection M}
    (hp : p ≤ P) (hq : q ≤ Q) (he : p.Equivalent q) (h : P.Subequivalent Q) :
    (remainder p P hp).Subequivalent (remainder q Q hq) := by
…
```
Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.AlgebraProjection.remainder, OAI.Generator.Tracial.AlgebraProjection.Subequivalent
theorem OAI.Generator.Tracial.AlgebraProjection.remainder_equivalent line 788
theorem OAI.Generator.Tracial.PartialIsometry.exists_finsetSum line 806
theorem OAI.Generator.Tracial.AlgebraProjection.isStarProjection_sum line 837
def OAI.Generator.Tracial.AlgebraProjection.finsetSum line 846
theorem OAI.Generator.Tracial.AlgebraProjection.finsetSum_le_iff line 850
def OAI.Generator.Tracial.EquivalentPartition.subset line 870
theorem OAI.Generator.Tracial.EquivalentPartition.subset_val line 874
theorem OAI.Generator.Tracial.EquivalentPartition.subset_le_iff line 877
theorem OAI.Generator.Tracial.EquivalentPartition.subset_le line 881
theorem OAI.Generator.Tracial.EquivalentPartition.subset_mono line 884
theorem OAI.Generator.Tracial.EquivalentPartition.subset_univ line 888
theorem OAI.Generator.Tracial.EquivalentPartition.subset_empty line 891
theorem OAI.Generator.Tracial.EquivalentPartition.subset_singleton line 894
theorem OAI.Generator.Tracial.EquivalentPartition.subset_equivalent_of_equiv line 898
Source documentation
A bijection of subsets gives a sum of explicit matrix-unit links.
```
theorem subset_equivalent_of_equiv (E : EquivalentPartition p ι) (s t : Finset ι)
    (e : s ≃ t) : (E.subset s).Equivalent (E.subset t) := by
…
```
Mentions: OAI.Generator.Tracial.EquivalentPartition
theorem OAI.Generator.Tracial.EquivalentPartition.subset_equivalent_of_card_eq line 923
theorem OAI.Generator.Tracial.EquivalentPartition.subset_refine line 928
Source documentation
Subset sums stay compatible with refinement to all children.
```
theorem subset_refine {κ : Type*} [Fintype κ] (E : EquivalentPartition p ι)
    (F : EquivalentPartition E.base κ) (s : Finset ι) :
    (E.refine F).subset (s ×ˢ Finset.univ)=E.subset s := by
…
```
Mentions: OAI.Generator.Tracial.EquivalentPartition, OAI.Generator.Tracial.EquivalentPartition.subset
theorem OAI.Generator.Tracial.EquivalentPartition.subset_mul_piece_of_not_mem line 938
theorem OAI.Generator.Tracial.EquivalentPartition.subset_le_subset_iff line 943
theorem OAI.Generator.Tracial.EquivalentPartition.subset_subequivalent_of_card_le line 954

theorem OAI.Generator.Tracial.EquivalentPartition.subset_subequivalent_iff_card_le line 962

Source documentation

The witness-based comparison agrees exactly with cardinal comparison.

theorem subset_subequivalent_iff_card_le
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (E : EquivalentPartition p ι) (hp : p.val≠0) (s t : Finset ι) :
    (E.subset s).Subequivalent (E.subset t) ↔ s.card ≤ t.card := by
…

Mentions: OAI.Generator.Tracial.EquivalentPartition

theorem OAI.Generator.Tracial.EquivalentPartition.subset_equivalent_iff_card_eq line 981
theorem OAI.Generator.Tracial.EquivalentPartition.subset_orthogonal_of_disjoint line 992
theorem OAI.Generator.Tracial.EquivalentPartition.subset_union line 1001
theorem OAI.Generator.Tracial.EquivalentPartition.subset_insert line 1007