OAI/Analysis/JiangSu/DimensionDrop/DimensionDropPartitionWeights.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.JiangSuConstruction.realScalarDrop line 19
  2. lemma OAI.JiangSuConstruction.realScalarDrop_commute line 29
  3. lemma OAI.JiangSuConstruction.realScalarDrop_selfAdjoint line 36
  4. lemma OAI.JiangSuConstruction.realScalarDrop_sum line 43
  5. def OAI.JiangSuConstruction.realSqrtMap line 53
  6. lemma OAI.JiangSuConstruction.realScalarDrop_sqrt_sq line 56
  7. lemma OAI.JiangSuConstruction.realScalarDrop_tensor_commute line 63
  8. lemma OAI.JiangSuConstruction.tensor_cstar_one_le line 73
  9. lemma OAI.JiangSuConstruction.partition_tensor_bound line 79
  10. abbrev OAI.JiangSuConstruction.dropEvaluation line 108
  11. def OAI.JiangSuConstruction.partitionInterpolate line 111
  12. lemma OAI.JiangSuConstruction.partitionInterpolate_apply line 117
  13. lemma OAI.JiangSuConstruction.partitionInterpolate_error line 127
  14. lemma OAI.JiangSuConstruction.partitionInterpolate_tensor line 155
  15. lemma OAI.JiangSuConstruction.dimensionDrop_tensor_bound_sum line 173
  16. lemma OAI.JiangSuConstruction.dimensionDrop_tensor_bound line 220
  17. theorem OAI.JiangSuConstruction.dimensionDrop_nuclear line 226