OAI/Analysis/PureInfiniteness/SpectralCopies.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Disjoint copies of a spectral return column. These encode the finite amplification in KR02 Lemmas 7.8 and 7.10.

  1. def OAI.WeakPureInfiniteness.supportedSpectralCopy line 17
  2. lemma OAI.WeakPureInfiniteness.sum_supportedSpectralCopy line 20
  3. lemma OAI.WeakPureInfiniteness.sum_smul_supportedSpectralCopy line 24
  4. lemma OAI.WeakPureInfiniteness.supportedSpectralCopy_support line 29
  5. lemma OAI.WeakPureInfiniteness.supportedSpectralCopy_disjoint line 34
  6. lemma OAI.WeakPureInfiniteness.supportedSpectralCopy_nonneg line 46
  7. lemma OAI.WeakPureInfiniteness.sqrt_supportedSpectralCopy line 51
  8. lemma OAI.WeakPureInfiniteness.spectralCopies_cross_diagonal_zero line 62