OAI/Analysis/JiangSu/CStarAlgebras/SmoothedIntegerCuts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Pureness.smoothedIntegerCutCount line 10
  2. lemma OAI.Pureness.smoothedIntegerCutCount_nonneg line 13
  3. theorem OAI.Pureness.smoothedIntegerCutCount_bounds line 17
  4. def OAI.Pureness.positiveIntegerCut line 63
  5. lemma OAI.Pureness.positiveIntegerCut_nonneg line 66
  6. lemma OAI.Pureness.positiveIntegerCut_eq_posPart line 69
  7. lemma OAI.Pureness.spectralApproxUnit_positiveIntegerCut line 78
  8. lemma OAI.Pureness.smoothedIntegerCut_cfc line 85
  9. lemma OAI.Pureness.smoothedIntegerCut_operator_bounds line 102
  10. lemma OAI.Pureness.spectralApproxUnit_trace_tendsto_realRank line 144
  11. theorem OAI.Pureness.actual_spectral_integer_approximation line 153