OAI/Analysis/PureInfiniteness/SpectralCharacters.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Evaluation of the finite spectral partition at characters. These formulas reduce the joint estimates to their scalar versions without spectral measures.

  1. def OAI.WeakPureInfiniteness.spectralCharacter line 17
  2. lemma OAI.WeakPureInfiniteness.scalarStarHom_eq_real line 20
  3. lemma OAI.WeakPureInfiniteness.scalarStarHom_cfc line 28
  4. lemma OAI.WeakPureInfiniteness.norm_le_of_spectralCharacters line 36
  5. lemma OAI.WeakPureInfiniteness.scalarStarHom_productGridHat line 44
  6. lemma OAI.WeakPureInfiniteness.scalarStarHom_productGridPlateau line 56
  7. lemma OAI.WeakPureInfiniteness.norm_productGridHatElement_le_one line 68
  8. lemma OAI.WeakPureInfiniteness.norm_productGridPlateauElement_le_one line 78