OAI/Analysis/JiangSu/DimensionDrop/UniqueTrace.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.JiangSuConstruction.scalarDrop_norm_le line 14
  2. lemma OAI.JiangSuConstruction.scalarDrop_sub line 23
  3. lemma OAI.JiangSuConstruction.scalarDrop_const line 29
  4. lemma OAI.JiangSuConstruction.dimensionDrop_trace_oscillation line 34
  5. lemma OAI.JiangSuConstruction.primeDropLimit_trace_stage_unique line 52
  6. theorem OAI.JiangSuConstruction.primeDropLimit_trace_unique line 103
  7. lemma OAI.SequentialCStar.bounded_scalar_ultrafilter_tendsto line 139
  8. def OAI.SequentialCStar.familyTraceValue line 149
  9. lemma OAI.SequentialCStar.familyTraceValue_tendsto line 154
  10. def OAI.SequentialCStar.familyTraceLinear line 158
  11. lemma OAI.SequentialCStar.familyTraceLinear_norm line 169
  12. lemma OAI.SequentialCStar.familyTraceLinear_vanishing line 173
  13. def OAI.SequentialCStar.quotientTraceLinear line 182
  14. lemma OAI.SequentialCStar.quotientTraceLinear_mk line 185
  15. lemma OAI.SequentialCStar.quotientTraceLinear_norm line 188
  16. def OAI.SequentialCStar.quotientTrace line 194
  17. lemma OAI.SequentialCStar.quotientTrace_normalized line 197
  18. lemma OAI.SequentialCStar.quotientTrace_tracial line 204
  19. def OAI.SequentialCStar.limitTrace line 216
  20. lemma OAI.SequentialCStar.limitTrace_normalized line 219
  21. lemma OAI.SequentialCStar.limitTrace_tracial line 220
  22. lemma OAI.SequentialCStar.limitTrace_norm line 223