OAI/Analysis/FactorGeneration/NormalTrace.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

A genuine linear state with exact equality of real quadratic values, constructed from the original finite factor predicates by scalar compactness.

  1. theorem OAI.Generator.Tracial.exists_real_quadratic_state line 30
  2. theorem OAI.Generator.Tracial.exists_tracial_state line 76
  3. theorem OAI.Generator.Tracial.algebraProjection_nonneg line 104
  4. theorem OAI.Generator.Tracial.tracialFunctional_equivalent line 110
  5. theorem OAI.Generator.Tracial.positiveFunctional_projection_mono line 117
  6. theorem OAI.Generator.Tracial.tracialFunctional_subequivalent line 126
  7. theorem OAI.Generator.Tracial.tracialFunctional_dyadic_subset_re line 142
  8. theorem OAI.Generator.Tracial.tracialFunctional_projection_dimension_re line 165
  9. theorem OAI.Generator.Tracial.tracialFunctional_projection_dimension line 185
  10. theorem OAI.Generator.Tracial.functional_isDimensionSpectralValue line 219
  11. theorem OAI.Generator.Tracial.functional_eq_dimensionSpectralValue line 230
  12. theorem OAI.Generator.Tracial.dimensionSpectralValue_add line 239

    Source documentation

    The missing noncommuting additivity law, from the constructed linear state.

    theorem dimensionSpectralValue_add (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    (x y : M.toStarSubalgebra) (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :
    dimensionSpectralValue hfactor hdiff hfinite hunit (x+y) (hx.add hy)=
      dimensionSpectralValue hfactor hdiff hfinite hunit x hx+
      dimensionSpectralValue hfactor hdiff hfinite hunit y hy := by
…

    Mentions: OAI.Generator.Tracial.dimensionSpectralValue

  13. theorem OAI.Generator.Tracial.tracialFunctional_faithful line 251
  14. def OAI.Generator.Tracial.traceFreeTrace line 285
  15. theorem OAI.Generator.Tracial.traceFreeTrace_spec line 288
  16. theorem OAI.Generator.Tracial.traceFreeTrace_projection line 298
  17. theorem OAI.Generator.Tracial.traceFreeTrace_selfAdjoint line 303
  18. theorem OAI.Generator.Tracial.traceFreeTrace_faithful line 310
  19. theorem OAI.Generator.Tracial.traceFreeTrace_projection_tendsto line 315
  20. theorem OAI.Generator.Tracial.traceFreeTrace_matrix_diagonal line 346
  21. theorem OAI.Generator.Tracial.traceFreeTrace_exists_finite_vector_domination line 361
  22. theorem OAI.Generator.Tracial.traceFreeTrace_norm_sq_le line 394

    Source documentation

    The scalar Cauchy--Schwarz bound follows from positivity of a centered square.

    theorem traceFreeTrace_norm_sq_le (x : M.toStarSubalgebra) :
    ‖traceFreeTrace hfactor hdiff hfinite hunit x‖^2 ≤
      (traceFreeTrace hfactor hdiff hfinite hunit (star x*x)).re := by
…

    Mentions: OAI.Generator.Tracial.traceFreeTrace

  23. theorem OAI.Generator.Tracial.traceFreeTrace_finite_vector_representation line 435
  24. theorem OAI.Generator.Tracial.traceFreeTrace_normal line 462