OAI/Analysis/FactorGeneration/QuotientHilbert.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

The actual trace Hilbert completion of the bounded-sequence tracial quotient. The vector-trace representation is explicit data; its existence for an arbitrary factor is not asserted here. No free-independence premise occurs.

  1. abbrev OAI.Generator.Tracial.Q line 20
  2. theorem OAI.Generator.Tracial.trace_add line 22
  3. theorem OAI.Generator.Tracial.trace_smul line 34
  4. def OAI.Generator.Tracial.traceLinear line 43
  5. theorem OAI.Generator.Tracial.trace_pair line 48
  6. theorem OAI.Generator.Tracial.trace_pair_conj line 55
  7. theorem OAI.Generator.Tracial.trace_square_nonneg line 71
  8. theorem OAI.Generator.Tracial.norm₂_tendsto line 84

    Source documentation

    The quotient two-norm is the ultralimit of the coordinate two-norms.

    theorem norm₂_tendsto (a : Bounded M) :
    Tendsto (fun n => τ.norm₂ (a.val n)) (ω : Filter ℕ)
      (𝓝 (Real.sqrt (quotientTrace τ ω (star (quotientMap τ (ω : Filter ℕ) a) *
        quotientMap τ (ω : Filter ℕ) a)).re)) := by
…
  9. theorem OAI.Generator.Tracial.trace_square_faithful line 97
  10. def OAI.Generator.Tracial.quotientInnerCore line 109

    Source documentation

    The norm here is the trace norm, not the operator norm.

    @[instance_reducible] def quotientInnerCore : InnerProductSpace.Core ℂ (Q τ ω) where
…

    Mentions: OAI.Generator.Tracial.Q

  11. instance OAI.Generator.Tracial.quotientNormedAddCommGroup line 117
  12. instance OAI.Generator.Tracial.quotientInnerProductSpace line 119
  13. theorem OAI.Generator.Tracial.inner_eq_trace line 122
  14. abbrev OAI.Generator.Tracial.L2 line 126

    Source documentation

    Genuine complete complex Hilbert space for the quotient trace.

    abbrev L2 := UniformSpace.Completion (Q τ ω)

    Mentions: OAI.Generator.Tracial.Q

  15. def OAI.Generator.Tracial.inclusion line 128
  16. theorem OAI.Generator.Tracial.inclusion_inner line 131
  17. theorem OAI.Generator.Tracial.inclusion_injective line 135
  18. def OAI.Generator.Tracial.boundedScalarTrace line 150
  19. def OAI.Generator.Tracial.boundedCenter line 158
  20. theorem OAI.Generator.Tracial.boundedCenter_trace line 160
  21. theorem OAI.Generator.Tracial.boundedCenter_quotient line 166
  22. theorem OAI.Generator.Tracial.exists_centered_contraction_representative line 182
  23. theorem OAI.Generator.Tracial.quotient_norm_one line 212
  24. theorem OAI.Generator.Tracial.quotient_norm_star line 216
  25. theorem OAI.Generator.Tracial.quotient_trace_sub line 221
  26. theorem OAI.Generator.Tracial.quotient_norm_mul_unitary line 225
  27. theorem OAI.Generator.Tracial.quotient_trace_cauchy_schwarz line 235
  28. theorem OAI.Generator.Tracial.quotient_correlation_remainder line 241

    Source documentation

    The source's complex trace error bound from its actual first-order identity and the actual quotient remainder, with unitary right multiplication accounted for.

    theorem quotient_correlation_remainder (ξ v c w : Q τ ω) (target : ℂ) (R : ℝ)
    (hw : w*star w = 1)
    (hfirst : quotientTrace τ ω (star ξ*((1+c)*w)) = target)
    (hrem : ‖v-(1+c)‖ ≤ R) :
    ‖quotientTrace τ ω (star ξ*(v*w))-target‖ ≤ ‖ξ‖*R := by
…

    Mentions: OAI.Generator.Tracial.Q