Main.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Weak pure infiniteness and Cuntz-algebra absorption

Individual proper infiniteness implies strong pure infiniteness for arbitrary, possibly nonunital complex C*-algebras. Exactness removes a fixed finite amplification. The rectangular epsilon formulation of Cuntz comparison agrees with its sequential formulation.

def OAI.WeakPureInfiniteness.Campaign.FixedAmplification line 29
Source documentation
Fixed-amplification proper infiniteness, including the zero element.
```
def FixedAmplification (A : Type u) [NonUnitalCStarAlgebra A] (n : ℕ) : Prop :=
…
```
theorem OAI.WeakPureInfiniteness.Campaign.weaklyPurelyInfinite_iff line 33
Source documentation
Omitting zero does not change the fixed-amplification hypothesis.
```
theorem weaklyPurelyInfinite_iff :
    WeaklyPurelyInfinite A ↔ ∃ n : ℕ, 1 ≤ n ∧ FixedAmplification A n := by
…
```
Mentions: OAI.WeakPureInfiniteness.WeaklyPurelyInfinite, OAI.WeakPureInfiniteness.Campaign.FixedAmplification
theorem OAI.WeakPureInfiniteness.Campaign.finiteCuntzLE_iff line 42
Source documentation
Epsilon and sequential rectangular Cuntz comparison agree.
```
theorem finiteCuntzLE_iff {m n : ℕ}
    (a : CStarMatrix (Fin m) (Fin m) A)
    (b : CStarMatrix (Fin n) (Fin n) A) :
    MainGap.FiniteCuntzLE a b ↔ CuntzSubequiv a b := by
…
```
Mentions: OAI.MainGap.FiniteCuntzLE, OAI.WeakPureInfiniteness.CuntzSubequiv
theorem OAI.WeakPureInfiniteness.Campaign.scalarCorner_eq line 48
theorem OAI.WeakPureInfiniteness.Campaign.properlyInfinite_to_mainGap line 55
Source documentation
Translate the two-copy comparison without adding an exactness hypothesis.
```
theorem properlyInfinite_to_mainGap {a : A}
    (h : ProperlyInfinite (diagonalCopies 1 a)) : MainGap.ProperlyInfinite a := by
…
```
Mentions: OAI.WeakPureInfiniteness.ProperlyInfinite, OAI.WeakPureInfiniteness.diagonalCopies, OAI.MainGap.ProperlyInfinite
theorem OAI.WeakPureInfiniteness.Campaign.individual_to_strong line 65
Source documentation
Theorem 1.1: arbitrary positive diagonals and an arbitrary mixed entry.
```
theorem individual_to_strong
    (hP : FixedAmplification A 1) :
    MainGap.UnrestrictedDiagonalization A ∧ StronglyPurelyInfinite A := by
…
```
Mentions: OAI.WeakPureInfiniteness.Campaign.FixedAmplification, OAI.MainGap.UnrestrictedDiagonalization, OAI.WeakPureInfiniteness.StronglyPurelyInfinite
theorem OAI.WeakPureInfiniteness.Campaign.exact_fixedAmplification line 75
Source documentation
Theorem 1.2: exactness removes the fixed finite amplification.
```
theorem exact_fixedAmplification (hExact : Exact A) {n : ℕ} (hn : 1 ≤ n)
    (hF : FixedAmplification A n) :
    FixedAmplification A 1 ∧ MainGap.UnrestrictedDiagonalization A ∧
      StronglyPurelyInfinite A := by
…
```
Mentions: OAI.WeakPureInfiniteness.Exact, OAI.WeakPureInfiniteness.Campaign.FixedAmplification, OAI.MainGap.UnrestrictedDiagonalization, OAI.WeakPureInfiniteness.StronglyPurelyInfinite
theorem OAI.WeakPureInfiniteness.Campaign.nuclear_fixedAmplification line 85
Source documentation
The nuclear specialization, with no separability or unit assumption.
```
theorem nuclear_fixedAmplification (hNuclear : Nuclear A) {n : ℕ} (hn : 1 ≤ n)
    (hF : FixedAmplification A n) :
    FixedAmplification A 1 ∧ MainGap.UnrestrictedDiagonalization A ∧
      StronglyPurelyInfinite A :=
…
```
Mentions: OAI.WeakPureInfiniteness.Nuclear, OAI.WeakPureInfiniteness.Campaign.FixedAmplification, OAI.MainGap.UnrestrictedDiagonalization, OAI.WeakPureInfiniteness.StronglyPurelyInfinite
theorem OAI.WeakPureInfiniteness.Campaign.nuclear_absorption_conditional line 92
Source documentation
Corollary 1.3, conditional only on the cited published absorption input.
```
theorem nuclear_absorption_conditional [TopologicalSpace.SeparableSpace A]
    (hKirchberg : KirchbergOInfinityAbsorption A)
    (hNuclear : Nuclear A) {n : ℕ} (hn : 1 ≤ n)
    (hF : FixedAmplification A n) :
    AbsorbsOInfinity A := by
…
```
Mentions: OAI.WeakPureInfiniteness.KirchbergOInfinityAbsorption, OAI.WeakPureInfiniteness.Nuclear, OAI.WeakPureInfiniteness.Campaign.FixedAmplification, OAI.WeakPureInfiniteness.AbsorbsOInfinity