OAI/Analysis/TraceCone/StrongConvergence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TraceConeClassification.positive_op_square_le line 20
2. lemma OAI.TraceConeClassification.positive_op_normsq_le line 30
3. lemma OAI.TraceConeClassification.positive_contraction_error line 42
4. lemma OAI.TraceConeClassification.operator_inner_mono line 59
5. lemma OAI.TraceConeClassification.monotone_operator_cauchy line 67

   Source documentation

   Bounded monotone nets of positive operators are strongly Cauchy. This allows arbitrary directed index sets, not only sequences or countable weights.

   lemma monotone_operator_cauchy (T : ι → H →L[ℂ] H) (hT : Monotone T)
       (hpos : ∀ i, 0 ≤ T i) (a : H →L[ℂ] H) (ha : ∀ i, T i ≤ a) (ξ : H) :
       CauchySeq (fun i => T i ξ) := by
   …

6. lemma OAI.TraceConeClassification.monotone_operator_strong_limit line 114
7. lemma OAI.TraceConeClassification.strong_limit_nonneg line 134

   Source documentation

   Positivity is closed along actual strong-operator limits.

   lemma strong_limit_nonneg {κ : Type*} {l : Filter κ} [l.NeBot]
       (T : κ → H →L[ℂ] H) (S : H →L[ℂ] H)
       (hlim : ∀ ξ, Tendsto (fun i => T i ξ) l (𝓝 (S ξ))) (hpos : ∀ᶠ i in l, 0 ≤ T i) : 0 ≤ S := by
   …

8. lemma OAI.TraceConeClassification.bicommutant_strong_net line 159

   Source documentation

   An actual strong-operator approximating net, with the finite-set index written explicitly. No first-countability of the operator topology is used.

   lemma bicommutant_strong_net (C : StarSubalgebra ℂ (H →L[ℂ] H)) (T : H →L[ℂ] H)
       (hT : T ∈ Set.centralizer (Set.centralizer (C : Set (H →L[ℂ] H)))) :
       ∃ a : Finset H × ℕ → H →L[ℂ] H, (∀ p, a p ∈ C) ∧
         ∀ ξ, Tendsto (fun p => a p ξ) atTop (𝓝 (T ξ)) := by
   …