OAI/Analysis/Nuclearity/NuclearUnitizationCPAP.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Matrix approximations of the unitization. An extra matrix block records the scalar coordinate, so the return map fixes the adjoined unit exactly.

  1. abbrev OAI.WeakPureInfiniteness.Mat line 17
  2. abbrev OAI.WeakPureInfiniteness.Block line 18
  3. def OAI.WeakPureInfiniteness.scalarMatrixHom line 33
  4. def OAI.WeakPureInfiniteness.unitizedMatrixCompression line 36
  5. def OAI.WeakPureInfiniteness.unitizedMatrixReturn line 42
  6. lemma OAI.WeakPureInfiniteness.scalarMatrixHom_entry line 50
  7. lemma OAI.WeakPureInfiniteness.unitizedMatrixCompression_apply line 54
  8. lemma OAI.WeakPureInfiniteness.unitizedMatrixReturn_apply line 59
  9. lemma OAI.WeakPureInfiniteness.unitizedMatrixCompression_cp line 63
  10. lemma OAI.WeakPureInfiniteness.unitizedMatrixCompression_one line 73
  11. lemma OAI.WeakPureInfiniteness.unitizedMatrixReturn_cp line 87
  12. lemma OAI.WeakPureInfiniteness.unitizedMatrixReturn_one line 96
  13. lemma OAI.WeakPureInfiniteness.unitizedMatrixReturn_compression line 102
  14. lemma OAI.WeakPureInfiniteness.clm_comp_norm_le_one line 121
  15. theorem OAI.WeakPureInfiniteness.nuclear_unitization_cpap line 130

    Source documentation

    Nuclear matrix approximations extend to the forced unitization.

    theorem nuclear_unitization_cpap (hA : Nuclear A) : Nuclear (Unitization ℂ A) := by
…

    Mentions: OAI.WeakPureInfiniteness.Nuclear