OAI/Analysis/FactorGeneration/PartialUnitaries.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Popa's extension order on actual supported partial unitaries, and its exact L2 distance identity.

  1. structure OAI.Generator.Tracial.PartialUnitary line 19
  2. abbrev OAI.Generator.Tracial.PartialUnitary.val line 24
  3. def OAI.Generator.Tracial.PartialUnitary.Extends line 26
  4. theorem OAI.Generator.Tracial.PartialUnitary.support_le_of_extends line 28
  5. theorem OAI.Generator.Tracial.PartialUnitary.cross_initial line 37
  6. theorem OAI.Generator.Tracial.PartialUnitary.cross_initial_rev line 42
  7. theorem OAI.Generator.Tracial.PartialUnitary.left_extends line 47
  8. theorem OAI.Generator.Tracial.PartialUnitary.extends_refl line 52
  9. theorem OAI.Generator.Tracial.PartialUnitary.extends_trans line 54
  10. theorem OAI.Generator.Tracial.PartialUnitary.ext line 61
  11. instance OAI.Generator.Tracial.PartialUnitary.(instance at line 76) line 76
  12. theorem OAI.Generator.Tracial.PartialUnitary.support_mono line 87
  13. theorem OAI.Generator.Tracial.PartialUnitary.difference_square line 90
  14. theorem OAI.Generator.Tracial.PartialUnitary.distance_sq line 95
  15. theorem OAI.Generator.Tracial.PartialUnitary.support_trace_mono line 101
  16. theorem OAI.Generator.Tracial.PartialUnitary.support_trace_le_one line 120
  17. theorem OAI.Generator.Tracial.PartialUnitary.monotone_cauchy line 125
  18. theorem OAI.Generator.Tracial.PartialUnitary.of_L2_limit line 145

    Source documentation

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

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

    Mentions: OAI.Generator.Tracial.PartialUnitary, OAI.Generator.Tracial.PartialUnitary.val

  19. theorem OAI.Generator.Tracial.PartialUnitary.le_of_eventually_le_limit line 172

    Source documentation

    A bounded L2 limit retains every eventually fixed extension.

    theorem le_of_eventually_le_limit (a : ℕ → PartialUnitary M) (v w : PartialUnitary 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.PartialUnitary, OAI.Generator.Tracial.PartialUnitary.val

  20. theorem OAI.Generator.Tracial.PartialUnitary.monotone_limit line 184
  21. theorem OAI.Generator.Tracial.PartialUnitary.eq_of_le_of_trace_eq line 203
  22. theorem OAI.Generator.Tracial.PartialUnitary.support_limit line 210
  23. theorem OAI.Generator.Tracial.PartialUnitary.support_trace_limit line 218
  24. theorem OAI.Generator.Tracial.PartialUnitary.limit_le_of_le line 223
  25. theorem OAI.Generator.Tracial.PartialUnitary.chain_limit line 236

    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 (PartialUnitary M)) (hc : IsChain (· ≤ ·) c) (hne : c.Nonempty) :
    ∃ (a : ℕ → PartialUnitary M) (v : PartialUnitary 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.PartialUnitary, OAI.Generator.Tracial.PartialUnitary.val

  26. def OAI.Generator.Tracial.dyadicSign line 291
  27. def OAI.Generator.Tracial.dyadicRademacher line 293
  28. theorem OAI.Generator.Tracial.dyadicRademacher_star line 296
  29. theorem OAI.Generator.Tracial.dyadicRademacher_sq line 304
  30. def OAI.Generator.Tracial.dyadicCornerUnitary line 314
  31. theorem OAI.Generator.Tracial.dyadicRademacher_centered_over_previous line 321

    Source documentation

    The next sign is centered even after multiplication by an arbitrary member of the previous finite dyadic algebra.

    theorem dyadicRademacher_centered_over_previous (p : AlgebraProjection M) (n : ℕ)
    (c : DyadicIndex n → ℂ) :
    τ.trace (dyadicEval τ hdiff p n c*dyadicRademacher τ hdiff p n)=0 := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.DyadicIndex, OAI.Generator.Tracial.dyadicEval, OAI.Generator.Tracial.dyadicRademacher

  32. theorem OAI.Generator.Tracial.dyadicRademacher_trace_mul_of_lt line 336
  33. theorem OAI.Generator.Tracial.dyadicRademacher_trace_mul_of_ne line 343
  34. theorem OAI.Generator.Tracial.coordinate_inner_eq_trace line 350
  35. theorem OAI.Generator.Tracial.dyadicRademacher_norm₂ line 355
  36. theorem OAI.Generator.Tracial.orthonormal_inner_tendsto_zero line 377

    Source documentation

    Bessel's inequality makes the coefficients of an orthonormal sequence vanish.

    theorem orthonormal_inner_tendsto_zero (v : ℕ → H) (hv : Orthonormal ℂ v) (x : H) :
    Tendsto (fun n => inner ℂ x (v n)) atTop (𝓝 0) := by
…
  37. theorem OAI.Generator.Tracial.dyadicRademacher_weak_trace_zero line 398
  38. theorem OAI.Generator.Tracial.dyadicRademacher_mixed_trace_zero line 424
  39. theorem OAI.Generator.Tracial.inclusion_corner_mixed_trace_zero line 435

    Source documentation

    The same sequence has vanishing ambient mixed traces, even when the coefficients belong to M and the partial unitaries belong to P.

    theorem inclusion_corner_mixed_trace_zero {P : VonNeumannAlgebra H} (hPM : P ≤ M)
    (hdiffP : ∀ p : P.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q : P.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p*q = q ∧ q*p = q)
    (p : AlgebraProjection P) (hp : p.val ≠ 0) (x y : M.toStarSubalgebra) :
    Tendsto (fun n => τ.trace (x*coordinateInclusion hPM
      (dyadicCornerUnitary (restrictedTrace τ hPM) hdiffP p n).val*y)) atTop (𝓝 0) := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.coordinateInclusion, OAI.Generator.Tracial.dyadicCornerUnitary, OAI.Generator.Tracial.restrictedTrace

  40. theorem OAI.Generator.Tracial.exists_cornerUnitary_small_mixed_traces line 451

    Source documentation

    Actual simultaneous scalar nonintertwining choices in every nonzero corner, with arbitrary finite sets of ambient left and right coefficients.

    theorem exists_cornerUnitary_small_mixed_traces {P : VonNeumannAlgebra H} (hPM : P ≤ M)
    (hdiffP : ∀ p : P.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q : P.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p*q = q ∧ q*p = q)
    (p : AlgebraProjection P) (hp : p.val ≠ 0)
    (F G : Finset M.toStarSubalgebra) (ε : ℝ) (hε : 0 < ε) :
    ∃ v : CornerUnitary p, ∀ x ∈ F, ∀ y ∈ G,
      ‖τ.trace (x*coordinateInclusion hPM v.val*y)‖ < ε := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.CornerUnitary, OAI.Generator.Tracial.coordinateInclusion