OAI/Analysis/JiangSu/Comparison/Ranks.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectComparison.directCutoff line 19
  2. def OAI.DirectComparison.directPositiveCut line 21
  3. lemma OAI.DirectComparison.directPositiveCut_nonneg line 23
  4. lemma OAI.DirectComparison.directCutoff_fixes_cut line 27
  5. lemma OAI.DirectComparison.hereditary_fixed_by_cutoff line 42
  6. theorem OAI.DirectComparison.directCutoff_fixes_hereditary line 57
  7. lemma OAI.DirectComparison.norm_sub_directPositiveCut_le line 71
  8. lemma OAI.DirectComparison.directPositiveCut_tendsto line 88
  9. theorem OAI.DirectComparison.rank_le_iSup_directPositiveCut line 98
  10. lemma OAI.DirectComparison.directPositiveCut_mem_hereditary line 105
  11. lemma OAI.DirectComparison.rank_directPositiveCut_le line 112
  12. lemma OAI.DirectComparison.directPositiveCut_shift line 118
  13. lemma OAI.DirectComparison.rank_directPositiveCut_antitone line 133
  14. theorem OAI.DirectComparison.rank_eq_iSup_directPositiveCut line 140
  15. lemma OAI.DirectComparison.directRank_ne_top line 156
  16. lemma OAI.DirectComparison.direct_isOpen_lt_rank line 160
  17. lemma OAI.DirectComparison.direct_isOpen_lt_realRank line 170
  18. theorem OAI.DirectComparison.uniform_direct_positive_cut line 185
  19. lemma OAI.DirectComparison.directPositiveCut_eq_traceConeCut line 224
  20. lemma OAI.DirectComparison.direct_rank_le_of_traceCone_comparison line 229
  21. lemma OAI.DirectComparison.direct_cut_rank_of_perturbation line 238
  22. theorem OAI.DirectComparison.direct_perturbed_cut_ranks line 248
  23. theorem OAI.DirectComparison.direct_cut_rank_star_mul_self line 264
  24. lemma OAI.DirectComparison.positive_contraction_defect_nonneg line 290
  25. lemma OAI.DirectComparison.directCutoff_nonneg line 307
  26. lemma OAI.DirectComparison.directCutoff_le_one line 312
  27. lemma OAI.DirectComparison.directCutoff_mem_hereditary line 315
  28. lemma OAI.DirectComparison.rank_le_trace_of_fixation line 321
  29. def OAI.DirectComparison.directSoftProjection line 334
  30. lemma OAI.DirectComparison.directSoftProjection_nonneg line 337
  31. lemma OAI.DirectComparison.directSoftProjection_norm_le line 341
  32. lemma OAI.DirectComparison.directSoftProjection_fixes line 346
  33. theorem OAI.DirectComparison.directSoftProjection_trace_bounds line 354
  34. lemma OAI.DirectComparison.directSoftProjection_mem_hereditary_of_mem line 397
  35. theorem OAI.DirectComparison.direct_scalar_almost_projection_step line 410