Basic.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Extended traces and positive cuts

We use the extended lower semicontinuous traces of The trace cone classifies Razak–Jacelon stabilizations, Sections 1 and 2. The finite domain need not be dense. Positive cuts are defined by nonunital continuous functional calculus, and canonical convergence is stated using filters.

abbrev OAI.TraceConeClassification.Positive line 29
Source documentation
The positive cone of the algebra, with its norm-subspace topology.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:12 (same declaration text).
```
abbrev Positive := {a : A // 0 ≤ a}
…
```
def OAI.TraceConeClassification.Positive.zero line 35
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:16 (same declaration text).
def OAI.TraceConeClassification.Positive.add line 36
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:17 (same declaration text).
def OAI.TraceConeClassification.Positive.scale line 37
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:18 (same declaration text).
def OAI.TraceConeClassification.Positive.starMul line 39
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:20 (same declaration text).
def OAI.TraceConeClassification.Positive.mulStar line 40
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:21 (same declaration text).
def OAI.TraceConeClassification.Positive.cut line 43
Source documentation
The nonunital positive cut (a - ε)₊, defined using functional calculus.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:22 (same declaration text).
```
def cut (a : Positive A) (ε : ℝ≥0) : Positive A :=
…
```
Mentions: OAI.TraceConeClassification.Positive
structure OAI.TraceConeClassification.ExtendedTrace line 50
Source documentation
Extended lower semicontinuous traces, with no finiteness restriction.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:27 (same declaration text).
```
structure ExtendedTrace where
…
```
instance OAI.TraceConeClassification.(instance at line 59) line 59
def OAI.TraceConeClassification.CanonicalConvergence line 65
Source documentation
Literal filter version of the manuscript's canonical convergence formula. Every directed net is covered by its tail filter.
Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:39 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.CanonicalConvergence@path.
```
def CanonicalConvergence {ι : Type*} (l : Filter ι) (τ : ι → ExtendedTrace A)
    (σ : ExtendedTrace A) : Prop :=
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
lemma OAI.TraceConeClassification.ExtendedTrace.monotone line 75
lemma OAI.TraceConeClassification.ExtendedTrace.map_scale_all line 83
lemma OAI.TraceConeClassification.Positive.cut_le line 98
lemma OAI.TraceConeClassification.Positive.norm_cut_sub_le line 106
lemma OAI.TraceConeClassification.Positive.tendsto_cut_reciprocal line 126
theorem OAI.TraceConeClassification.trace_eq_iSup_positive_cuts line 136
Source documentation
Lower semicontinuity recovers a trace value from its positive cuts.
```
theorem trace_eq_iSup_positive_cuts (τ : ExtendedTrace A) (a : Positive A) :
    τ a = ⨆ (ε : ℝ≥0) (_ : 0 < ε), τ (Positive.cut a ε) := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.Positive, OAI.TraceConeClassification.Positive.cut
def OAI.TraceConeClassification.positiveCut line 151
def OAI.TraceConeClassification.CuntzSubequivalent line 153
def OAI.TraceConeClassification.cutTransfer line 158
Source documentation
A continuous extension of the manuscript's gδ away from the nonnegative spectrum. The denominator is never zero when δ>0.
```
def cutTransfer (δ t : ℝ) : ℝ := Real.sqrt (max (t - δ) 0 / max t δ)
```
lemma OAI.TraceConeClassification.cutTransfer_continuous line 160
lemma OAI.TraceConeClassification.cutTransfer_zero line 166
lemma OAI.TraceConeClassification.cutTransfer_sq line 169
lemma OAI.TraceConeClassification.cutTransfer_eq_source line 173
lemma OAI.TraceConeClassification.cutTransfer_product line 180
lemma OAI.TraceConeClassification.cutTransfer_bound line 189
lemma OAI.TraceConeClassification.cutTransfer_cfc_product line 194
lemma OAI.TraceConeClassification.cutTransfer_cfc_bound line 212
def OAI.TraceConeClassification.Positive.conjugate line 238
Source documentation
Positive conjugation inside the same (possibly nonunital) C*-algebra.
```
def conjugate (x : A) (b : Positive A) : Positive A :=
…
```
Mentions: OAI.TraceConeClassification.Positive
lemma OAI.TraceConeClassification.ExtendedTrace.conjugate_le line 245
lemma OAI.TraceConeClassification.ExtendedTrace.conjugate_finite line 268
theorem OAI.TraceConeClassification.trace_cut_finite_of_near_finite line 275
Source documentation
A necessary finite-domain consequence of positive norm-cut comparison.
```
theorem trace_cut_finite_of_near_finite (τ : ExtendedTrace A) (a b : Positive A)
    (ε : ℝ≥0) (hε : 0 < ε) (hab : ‖a.1 - b.1‖ < ε) (hb : τ b < ∞) :
    τ (Positive.cut a ε) < ∞ := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.Positive, OAI.TraceConeClassification.Positive.cut
def OAI.TraceConeClassification.ExtendedTrace.scale line 314
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:48 (same declaration text).
lemma OAI.TraceConeClassification.ExtendedTrace.scale_apply line 324