OAI/Analysis/PureInfiniteness/SpectralMaps.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Transport of the finite Gram data through the original algebra's unitization map. No pure-infiniteness assumption is imposed on the unitization.

  1. lemma OAI.WeakPureInfiniteness.map_sqrt_nonneg line 18
  2. lemma OAI.WeakPureInfiniteness.rectangularMap_gram_cut line 23
  3. lemma OAI.WeakPureInfiniteness.rectangularMap_row_factor line 35
  4. lemma OAI.WeakPureInfiniteness.rectangularMap_relative_offdiagonal line 43