OAI/Analysis/JiangSu/DimensionDrop/Separable.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.JiangSuConstruction.spectralTransfer_re line 18
  2. lemma OAI.JiangSuConstruction.spectralTransfer_re_lower_bound line 25
  3. lemma OAI.JiangSuConstruction.spectralTransfer_re_lower line 37
  4. lemma OAI.JiangSuConstruction.spectralTransfer_re_upper line 49
  5. lemma OAI.JiangSuConstruction.scalarIterates_re_lower_bound line 61
  6. lemma OAI.JiangSuConstruction.scalarIterates_shift line 67
  7. lemma OAI.JiangSuConstruction.scalarIterates_re_net line 86
  8. lemma OAI.JiangSuConstruction.scalarIterates_add line 139
  9. theorem OAI.JiangSuConstruction.scalarIterates_eventually_positive line 154
  10. theorem OAI.JiangSuConstruction.scalarIterates_eventually_oscillation line 179