OAI/Analysis/FactorGeneration/ProjectionEncoding.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

A separated idempotent is recovered from commutation with a norm-small perturbation. This is an elementary substitute for the spectral-cut step.

  1. theorem OAI.Generator.offDiagonal_eq_zero_of_gap line 20
  2. theorem OAI.Generator.commute_projection_of_gap line 55
  3. def OAI.Generator.CommutingProjectionEncoding.weight line 84
  4. theorem OAI.Generator.CommutingProjectionEncoding.weight_nonneg line 86
  5. theorem OAI.Generator.CommutingProjectionEncoding.weight_hasSum line 88
  6. def OAI.Generator.CommutingProjectionEncoding.tail line 96
  7. theorem OAI.Generator.CommutingProjectionEncoding.term_norm_le line 101
  8. theorem OAI.Generator.CommutingProjectionEncoding.tail_summable line 105
  9. theorem OAI.Generator.CommutingProjectionEncoding.tail_norm_le line 108
  10. theorem OAI.Generator.CommutingProjectionEncoding.tail_step line 111
  11. theorem OAI.Generator.CommutingProjectionEncoding.tail_selfAdjoint line 115
  12. theorem OAI.Generator.CommutingProjectionEncoding.tail_mem line 120
  13. theorem OAI.Generator.CommutingProjectionEncoding.projection_commutes_tail line 131
  14. theorem OAI.Generator.CommutingProjectionEncoding.projection_mem_of_tail_mem line 134
  15. theorem OAI.Generator.CommutingProjectionEncoding.projection_mem_wstar line 152
  16. theorem OAI.Generator.CommutingProjectionEncoding.wstar_encoding line 169
  17. theorem OAI.Generator.CommutingProjectionEncoding.exists_selfAdjoint_generator line 181

    Source documentation

    Countable commuting-projection encoding without additional structural hypotheses.

    theorem exists_selfAdjoint_generator :
    ∃ b : (H →L[ℂ] H), IsSelfAdjoint b ∧ ‖b‖ ≤ 1 ∧ wstar {b}=wstar (Set.range e) :=
…

    Mentions: OAI.Generator.wstar

  18. theorem OAI.Generator.idempotent_mem_wstar_of_gap line 191