OAI/Analysis/FactorGeneration/ResidualCompletion.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Actual residual projections, null-set masking, and coordinatewise orthogonal partial-unitary patching.

  1. def OAI.Generator.Tracial.boundedPartialResidual line 19
  2. theorem OAI.Generator.Tracial.boundedPartialResidual_projection line 22
  3. theorem OAI.Generator.Tracial.boundedPartialResidual_mem line 25
  4. def OAI.Generator.Tracial.maskPartialSequence line 35
  5. theorem OAI.Generator.Tracial.maskPartialSequence_quotient line 38
  6. theorem OAI.Generator.Tracial.maskPartialSequence_mem line 54
  7. theorem OAI.Generator.Tracial.maskPartialSequence_orthogonal line 62
  8. def OAI.Generator.Tracial.patchPartialSequence line 74
  9. theorem OAI.Generator.Tracial.patchPartialSequence_bounded line 80
  10. theorem OAI.Generator.Tracial.patchPartialSequence_mem line 86
  11. theorem OAI.Generator.Tracial.exists_supported_centered_contraction_family line 102
  12. theorem OAI.Generator.Tracial.residual_quotient_increment_of_normalized_representatives line 125
  13. theorem OAI.Generator.Tracial.residual_quotient_increment_of_representatives line 179
  14. theorem OAI.Generator.Tracial.exists_residual_quotient_increment line 229
  15. theorem OAI.Generator.Tracial.quotient_projection_eq_zero_of_trace_re line 268
  16. theorem OAI.Generator.Tracial.quotient_unitary_of_zero_residual line 275
  17. theorem OAI.Generator.Tracial.quotient_patch_residual_bound line 291
  18. theorem OAI.Generator.Tracial.bounded_orthogonal_patch_supported line 324
  19. theorem OAI.Generator.Tracial.quotient_orthogonal_patch_supported line 349
  20. theorem OAI.Generator.Tracial.patchPartialSequence_extends line 372
  21. theorem OAI.Generator.Tracial.exact_residual_patch_of_centered_family line 391
  22. theorem OAI.Generator.Tracial.exists_exact_residual_patch line 431
  23. def OAI.Generator.Tracial.quotientResidualTrace line 481
  24. theorem OAI.Generator.Tracial.quotientResidualTrace_nonneg line 484
  25. theorem OAI.Generator.Tracial.exists_exact_residual_step line 503
  26. theorem OAI.Generator.Tracial.exists_exact_residual_iteration line 516
  27. theorem OAI.Generator.Tracial.quotient_trace_sub' line 558
  28. theorem OAI.Generator.Tracial.quotientResidualTrace_eq line 562
  29. theorem OAI.Generator.Tracial.quotient_partial_distance_sq line 568
  30. theorem OAI.Generator.Tracial.quotientResidualTrace_antitone line 584
  31. theorem OAI.Generator.Tracial.exists_coordinate_monotone_upper line 591
  32. theorem OAI.Generator.Tracial.quotient_geometric_upper_completion line 600