OAI/Analysis/PureInfiniteness/JointSpectralQuadratic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The mesh-independent square-error estimate for the sampled spectral row. It is the norm estimate needed before the fixed-cut diagonalization in KR02 Remark 7.5 and Lemma 7.6.

  1. def OAI.WeakPureInfiniteness.sampledQuadraticError line 14
  2. lemma OAI.WeakPureInfiniteness.map_sampledQuadraticError line 17
  3. lemma OAI.WeakPureInfiniteness.scalarStarHom_sampledQuadraticError line 25
  4. lemma OAI.WeakPureInfiniteness.norm_sum_sampledQuadraticError_le line 35