OAI/Analysis/FactorGeneration/MonotoneTrace.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Bounded positive monotone nets have actual least upper bounds in M. Every displayed vector-trace bound passes to the constructed bound.

  1. theorem OAI.Generator.Tracial.exists_monotone_positive_limit line 30
  2. theorem OAI.Generator.Tracial.ambient_trace_nonneg line 65
  3. theorem OAI.Generator.Tracial.ambient_trace_mono line 69
  4. theorem OAI.Generator.Tracial.ambient_sqrt_mem line 75
  5. theorem OAI.Generator.Tracial.ambient_eq_zero_of_trace_zero line 81
  6. theorem OAI.Generator.Tracial.ambient_lowerBound_nonpos_of_trace_tendsto_zero line 97

    Source documentation

    Any lower bound of a uniformly bounded positive sequence whose traces tend to zero is nonpositive. The sequence need not itself be monotone.

    theorem ambient_lowerBound_nonpos_of_trace_tendsto_zero
    (b : ℕ → M.toStarSubalgebra) (hpos : ∀ n, 0 ≤ (b n).val)
    (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ n, ‖b n‖ ≤ C)
    (ht : Tendsto (fun n => (τ.trace (b n)).re) atTop (𝓝 0))
    (c : M.toStarSubalgebra) (hc : ∀ n, c.val ≤ (b n).val) : c.val ≤ 0 := by
…
  7. def OAI.Generator.Tracial.ambientAbsoluteValue line 128
  8. theorem OAI.Generator.Tracial.ambientAbsoluteValue_nonneg line 131
  9. theorem OAI.Generator.Tracial.ambientAbsoluteValue_norm line 134
  10. theorem OAI.Generator.Tracial.ambientAbsoluteValue_norm₂ line 139
  11. theorem OAI.Generator.Tracial.ambientAbsoluteValue_trace_le_norm₂ line 151
  12. theorem OAI.Generator.Tracial.ambient_le_absoluteValue line 156
  13. theorem OAI.Generator.Tracial.ambient_neg_absoluteValue_le line 163
  14. theorem OAI.Generator.Tracial.norm₂_realPart_le line 172
  15. theorem OAI.Generator.Tracial.norm₂_imaginaryPart_le line 185
  16. def OAI.Generator.positiveResolvent line 202
  17. theorem OAI.Generator.positiveResolvent_continuousOn line 204
  18. theorem OAI.Generator.positiveResolvent_eq line 213
  19. theorem OAI.Generator.positiveResolvent_nonneg line 227
  20. theorem OAI.Generator.positiveResolvent_le_one line 234
  21. theorem OAI.Generator.positiveResolvent_mono line 240
  22. theorem OAI.Generator.positiveResolvent_le_self line 247
  23. theorem OAI.Generator.half_le_positiveResolvent line 262
  24. theorem OAI.Generator.positiveResolvent_norm_le_one line 276
  25. def OAI.Generator.Tracial.algebraPositiveResolvent line 292
  26. theorem OAI.Generator.Tracial.ambient_trace_finset_sum line 297
  27. theorem OAI.Generator.Tracial.ambient_trace_real_smul line 309
  28. theorem OAI.Generator.Tracial.exists_positive_trace_tail_majorants line 316