OAI/Analysis/FactorGeneration/Expectations.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

The orthogonal subalgebra representative of a self-adjoint ambient operator is constructed, with its operator norm bound.

  1. theorem OAI.Generator.Tracial.selfAdjoint_pairing_im line 19
  2. theorem OAI.Generator.Tracial.exists_selfAdjoint_expectation line 27
  3. theorem OAI.Generator.Tracial.TraceOrthogonal.add line 85
  4. theorem OAI.Generator.Tracial.TraceOrthogonal.sub line 89
  5. theorem OAI.Generator.Tracial.TraceOrthogonal.smul line 93
  6. theorem OAI.Generator.Tracial.TraceOrthogonal.eq_zero line 96
  7. theorem OAI.Generator.Tracial.exists_bounded_subalgebra_representative line 104
  8. theorem OAI.Generator.Tracial.subalgebra_representative_unique line 126
  9. def OAI.Generator.Tracial.conditionalExpectation line 135
  10. theorem OAI.Generator.Tracial.conditionalExpectation_mem line 138
  11. theorem OAI.Generator.Tracial.conditionalExpectation_bound line 141
  12. theorem OAI.Generator.Tracial.conditionalExpectation_orthogonal line 144
  13. theorem OAI.Generator.Tracial.conditionalExpectation_eq_of_orthogonal line 148
  14. theorem OAI.Generator.Tracial.conditionalExpectation_add line 155
  15. theorem OAI.Generator.Tracial.conditionalExpectation_smul line 164
  16. def OAI.Generator.Tracial.conditionalExpectationCLM line 170
  17. theorem OAI.Generator.Tracial.conditionalExpectation_fixed line 177
  18. theorem OAI.Generator.Tracial.conditionalExpectation_trace line 184
  19. theorem OAI.Generator.Tracial.conditionalExpectation_selfAdjoint line 190
  20. theorem OAI.Generator.Tracial.expectation_trace_adjoint line 206
  21. theorem OAI.Generator.Tracial.TraceOrthogonal.mul_left line 213
  22. theorem OAI.Generator.Tracial.TraceOrthogonal.mul_right line 217
  23. theorem OAI.Generator.Tracial.TraceOrthogonal.adjoint line 222
  24. theorem OAI.Generator.Tracial.conditionalExpectation_mul_left line 230
  25. theorem OAI.Generator.Tracial.conditionalExpectation_mul_right line 236
  26. theorem OAI.Generator.Tracial.conditionalExpectation_star line 242
  27. theorem OAI.Generator.Tracial.conditionalExpectation_pythagoras line 248
  28. theorem OAI.Generator.Tracial.conditionalExpectation_norm₂_le line 262
  29. theorem OAI.Generator.Tracial.negPart_mem_inside line 284
  30. theorem OAI.Generator.Tracial.conditionalExpectation_nonneg line 291
  31. theorem OAI.Generator.Tracial.conditionalExpectation_mono line 312
  32. theorem OAI.Generator.Tracial.conditionalExpectation_schwarz line 335
  33. theorem OAI.Generator.Tracial.conditionalExpectation_norm_le line 359
  34. theorem OAI.Generator.Tracial.conditionalExpectation_opNorm_le line 368
  35. theorem OAI.Generator.Tracial.conditionalExpectation_idempotent line 376
  36. theorem OAI.Generator.Tracial.conditionalExpectation_tower line 389
  37. theorem OAI.Generator.Tracial.conditionalExpectation_nested_energy line 403
  38. theorem OAI.Generator.Tracial.conditionalExpectation_nested_norm₂ line 411
  39. theorem OAI.Generator.Tracial.bounded_trace_limit_inside line 428
  40. theorem OAI.Generator.Tracial.decreasing_expectations_converge line 450
  41. theorem OAI.Generator.Tracial.decreasing_expectations_scalar_limit line 501
  42. theorem OAI.Generator.Tracial.decreasing_expectations_finite_centered_budget line 512