OAI/Analysis/TraceCone/FiniteIdeal.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Finite ideals of extended traces

For an extended trace, the norm closure of the square-integrable ideal is the closed ideal generated by the finite-trace positive elements. Positive elements belong to this ideal exactly when each positive cut has finite trace. This gives the scalar limit at zero in the canonical trace convergence of The trace cone classifies Razak–Jacelon stabilizations, Section 2.

  1. lemma OAI.TraceConeClassification.residual_norm_bound line 28

    Source documentation

    Approximate-unit estimate in the original nonunital algebra.

    lemma residual_norm_bound {x b e : A} (hb : 0 ≤ b)
    (hxb : star x * x ≤ b) (he : IsSelfAdjoint e) (he1 : ‖e‖ ≤ 1) :
    ‖x - x * e‖ ^ 2 ≤ 2 * ‖b - e * b‖ := by
…
  2. lemma OAI.TraceConeClassification.closed_ideal_mem_of_square_le line 55

    Source documentation

    A closed absorbing star ideal contains elements whose square is dominated by one of its positives.

    lemma closed_ideal_mem_of_square_le
    (I : NonUnitalStarSubalgebra ℂ A) (hI : IsClosed (I : Set A))
    (hleft : ∀ (x y : A), y ∈ I → x * y ∈ I)
    {x b : A} (hb : 0 ≤ b) (hxb : star x * x ≤ b) (hbI : b ∈ I) : x ∈ I := by
…
  3. theorem OAI.TraceConeClassification.closed_ideal_hereditary line 83

    Source documentation

    A closed two-sided star ideal is hereditary.

    theorem closed_ideal_hereditary
    (I : NonUnitalStarSubalgebra ℂ A) (hI : IsClosed (I : Set A))
    (hleft : ∀ (x y : A), y ∈ I → x * y ∈ I)
    (_hright : ∀ (x y : A), x ∈ I → x * y ∈ I)
    {a b : A} (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ∈ I) : a ∈ I := by
…
  4. lemma OAI.TraceConeClassification.closed_ideal_star_mul_mem_iff line 96
  5. theorem OAI.TraceConeClassification.closed_ideal_weight_exists line 106

    Source documentation

    The literal ideal weight ι_I of st:ideals, retaining all infinity values.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NonUnitalCStarAlgebra, PartialOrder, StarOrderedRing, NonUnitalStarSubalgebra, Complex, IsClosed, Membership.mem, HMul.hMul, Exists, OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.Positive, Eq, ENNReal, OAI.TraceConeClassification.ExtendedTrace.toFun, ite, LE.le, OfNat.ofNat, Classical.propDecidable, Top.top

    Proof uses: Iff, HAdd.hAdd, And, Iff.intro, And.intro, OAI.TraceConeClassification.closed_ideal_hereditary, Subtype.property, le_add_of_nonneg_right, le_add_of_nonneg_left, Submodule.add_mem, NonUnitalSubalgebra.toSubmodule, NonUnitalStarSubalgebra.toNonUnitalSubalgebra, And.left, And.right, Real, HSMul.hSMul, Submodule.smul_mem, NNReal, LT.lt, OAI.TraceConeClassification.Positive.scale and 64 more

    161 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:61 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.closed_ideal_weight_exists@path.

    Tactic trace: 67 steps

    Open to load the checked before-and-after goal states.

    theorem closed_ideal_weight_exists
    (I : NonUnitalStarSubalgebra ℂ A) (hI : IsClosed (I : Set A))
    (hleft : ∀ (x y : A), y ∈ I → x * y ∈ I)
    (hright : ∀ (x y : A), x ∈ I → x * y ∈ I) :
    ∃ τ : ExtendedTrace A, ∀ a : Positive A, τ a = if a.1 ∈ I then 0 else ∞ := by
…

    Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.Positive

  6. def OAI.TraceConeClassification.ExtendedTrace.finiteSquareSet line 172

    Source documentation

    The two-sided square-integrable ideal, before taking its norm closure.

    Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:70 (same declaration text).

    def finiteSquareSet : Set A := {x | τ (Positive.starMul x) < ∞}

    Mentions: OAI.TraceConeClassification.Positive.starMul

  7. lemma OAI.TraceConeClassification.ExtendedTrace.zero_mem_finiteSquareSet line 174

    Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:71 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.ExtendedTrace.zero_mem_finiteSquareSet@path.

  8. lemma OAI.TraceConeClassification.ExtendedTrace.star_mem_finiteSquareSet line 178

    Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:72 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.ExtendedTrace.star_mem_finiteSquareSet@path.

  9. lemma OAI.TraceConeClassification.ExtendedTrace.smul_mem_finiteSquareSet line 187

    Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:74 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.ExtendedTrace.smul_mem_finiteSquareSet@path.

  10. lemma OAI.TraceConeClassification.ExtendedTrace.add_mem_finiteSquareSet line 202

    Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:76 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.ExtendedTrace.add_mem_finiteSquareSet@path.

  11. lemma OAI.TraceConeClassification.ExtendedTrace.mul_mem_finiteSquareSet_left line 218

    Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:79 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.ExtendedTrace.mul_mem_finiteSquareSet_left@path.

  12. lemma OAI.TraceConeClassification.ExtendedTrace.mul_mem_finiteSquareSet_right line 230
  13. def OAI.TraceConeClassification.ExtendedTrace.finiteSquareAlgebra line 235

    Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:82 (same declaration text).

  14. def OAI.TraceConeClassification.ExtendedTrace.finiteIdeal line 244

    Source documentation

    The closed ideal generated by the finite-trace positive elements.

    Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:90 (same declaration text).

    def finiteIdeal : NonUnitalStarSubalgebra ℂ A := τ.finiteSquareAlgebra.topologicalClosure
  15. lemma OAI.TraceConeClassification.ExtendedTrace.isClosed_finiteIdeal line 246

    Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:91 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.ExtendedTrace.isClosed_finiteIdeal@path.

  16. lemma OAI.TraceConeClassification.ExtendedTrace.mul_mem_finiteIdeal_left line 249

    Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:92 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.ExtendedTrace.mul_mem_finiteIdeal_left@path.

  17. lemma OAI.TraceConeClassification.ExtendedTrace.mul_mem_finiteIdeal_right line 256

    Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:94 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.ExtendedTrace.mul_mem_finiteIdeal_right@path.

  18. lemma OAI.TraceConeClassification.ExtendedTrace.positive_mem_finiteIdeal_of_finite line 261
  19. lemma OAI.TraceConeClassification.ExtendedTrace.finiteIdeal_le_iff line 275
  20. lemma OAI.TraceConeClassification.ExtendedTrace.finite_positive_dense line 290
  21. lemma OAI.TraceConeClassification.ExtendedTrace.positive_mem_finiteIdeal_iff_cuts line 308
  22. lemma OAI.TraceConeClassification.tendsto_scale_zero_of_finite line 330

    Source documentation

    Positive scalar multiples of a finite trace value tend to zero.

    lemma tendsto_scale_zero_of_finite (τ : ExtendedTrace A) (a : Positive A)
    (ha : τ a < ∞) :
    Tendsto (fun r : ℝ≥0 => τ.scale r a) (𝓝[>] 0) (𝓝 0) := by
…

    Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.Positive

  23. theorem OAI.TraceConeClassification.finite_domain_ideal_and_scalar_limit line 341

    Source documentation

    Exact finite-domain ideal and its scalar-limit weight. Its universal property is the manuscript's closed ideal generated by the finite-trace positives.

    theorem finite_domain_ideal_and_scalar_limit (τ : ExtendedTrace A) :
    ∃ I : NonUnitalStarSubalgebra ℂ A,
      IsClosed (I : Set A) ∧
      (∀ (x y : A), y ∈ I → x * y ∈ I) ∧
      (∀ (x y : A), x ∈ I → x * y ∈ I) ∧
      (∀ J : NonUnitalStarSubalgebra ℂ A, IsClosed (J : Set A) →
        (∀ (x y : A), y ∈ J → x * y ∈ J) →
        (∀ (x y : A), x ∈ J → x * y ∈ J) →
        (I ≤ J ↔ ∀ a : Positive A, τ a < ∞ → a.1 ∈ J)) ∧
      (∀ a : Positive A, a.1 ∈ I ↔
        ∀ (ε : ℝ≥0), 0 < ε → τ (Positive.cut a ε) < ∞) ∧
      ∃ ω : ExtendedTrace A,
…

    Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.Positive, OAI.TraceConeClassification.Positive.cut