OAI/Analysis/FactorGeneration/PartialIsometries.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Actual partial isometries, allowing distinct initial and final projections, with the extension order and its exact trace distance.

  1. structure OAI.Generator.Tracial.PartialIsometry line 18
  2. theorem OAI.Generator.Tracial.PartialIsometry.mul_support line 25
  3. def OAI.Generator.Tracial.PartialIsometry.target line 33
  4. theorem OAI.Generator.Tracial.PartialIsometry.target_mul line 40
  5. def OAI.Generator.Tracial.PartialIsometry.adjoint line 44
  6. theorem OAI.Generator.Tracial.PartialIsometry.norm_le_one line 47
  7. theorem OAI.Generator.Tracial.PartialIsometry.trace_support_eq_target line 53
  8. def OAI.Generator.Tracial.PartialIsometry.Extends line 58
  9. theorem OAI.Generator.Tracial.PartialIsometry.support_le_of_extends line 60
  10. theorem OAI.Generator.Tracial.PartialIsometry.cross_initial line 80
  11. theorem OAI.Generator.Tracial.PartialIsometry.cross_initial_rev line 85
  12. theorem OAI.Generator.Tracial.PartialIsometry.extends_refl line 90
  13. theorem OAI.Generator.Tracial.PartialIsometry.extends_trans line 92
  14. theorem OAI.Generator.Tracial.PartialIsometry.ext line 99
  15. instance OAI.Generator.Tracial.PartialIsometry.(instance at line 111) line 111
  16. theorem OAI.Generator.Tracial.PartialIsometry.support_mono line 122
  17. theorem OAI.Generator.Tracial.PartialIsometry.difference_square line 125
  18. theorem OAI.Generator.Tracial.PartialIsometry.distance_sq line 130
  19. theorem OAI.Generator.Tracial.PartialIsometry.support_trace_mono line 136
  20. theorem OAI.Generator.Tracial.PartialIsometry.support_trace_le_one line 155
  21. theorem OAI.Generator.Tracial.PartialIsometry.monotone_cauchy line 160
  22. theorem OAI.Generator.Tracial.PartialIsometry.of_L2_limit line 180

    Source documentation

    Closedness of actual partial isometries in the operator norm unit ball for L2 convergence.

    theorem of_L2_limit (a : ℕ → PartialIsometry M) (b : M.toStarSubalgebra)
    (hb : Tendsto (fun n => τ.norm₂ ((a n).val-b)) atTop (𝓝 0)) :
    ∃ v : PartialIsometry M, v.val=b := by
…

    Mentions: OAI.Generator.Tracial.PartialIsometry

  23. theorem OAI.Generator.Tracial.PartialIsometry.le_of_eventually_le_limit line 201

    Source documentation

    A bounded L2 limit retains every eventually fixed extension.

    theorem le_of_eventually_le_limit (a : ℕ → PartialIsometry M) (v w : PartialIsometry M)
    (hv : Tendsto (fun n => τ.norm₂ ((a n).val-v.val)) atTop (𝓝 0))
    (hw : ∀ᶠ n in atTop, w ≤ a n) : w ≤ v := by
…

    Mentions: OAI.Generator.Tracial.PartialIsometry

  24. theorem OAI.Generator.Tracial.PartialIsometry.monotone_limit line 213
  25. theorem OAI.Generator.Tracial.PartialIsometry.eq_of_le_of_trace_eq line 232
  26. theorem OAI.Generator.Tracial.PartialIsometry.support_limit line 239
  27. theorem OAI.Generator.Tracial.PartialIsometry.support_trace_limit line 247
  28. theorem OAI.Generator.Tracial.PartialIsometry.limit_le_of_le line 252
  29. theorem OAI.Generator.Tracial.PartialIsometry.chain_limit line 265

    Source documentation

    A nonempty chain has a sequential L2 upper bound; no countability of the chain and no cyclicity of the trace vector are assumed.

    theorem chain_limit (c : Set (PartialIsometry M)) (hc : IsChain (· ≤ ·) c) (hne : c.Nonempty) :
    ∃ (a : ℕ → PartialIsometry M) (v : PartialIsometry M),
      (∀ n, a n ∈ c) ∧ Monotone a ∧ (∀ w ∈ c, w ≤ v) ∧
      Tendsto (fun n => τ.norm₂ ((a n).val-v.val)) atTop (𝓝 0) := by
…

    Mentions: OAI.Generator.Tracial.PartialIsometry

  30. def OAI.Generator.Tracial.PartialIsometry.zero line 315
  31. theorem OAI.Generator.Tracial.PartialIsometry.support_le_iff_mul line 317
  32. theorem OAI.Generator.Tracial.PartialIsometry.target_le_iff_mul line 330
  33. theorem OAI.Generator.Tracial.PartialIsometry.mul_eq_zero line 340
  34. theorem OAI.Generator.Tracial.PartialIsometry.orthogonal_reverse line 347
  35. def OAI.Generator.Tracial.PartialIsometry.patch line 352
  36. theorem OAI.Generator.Tracial.PartialIsometry.patch_target line 363
  37. theorem OAI.Generator.Tracial.PartialIsometry.le_patch line 378
  38. theorem OAI.Generator.Tracial.PartialIsometry.patch_ne line 387
  39. theorem OAI.Generator.Tracial.PartialIsometry.supports_of_L2_limit line 408
  40. theorem OAI.Generator.Tracial.PartialIsometry.exists_maximal_between line 432