OAI/Analysis/JiangSu/DimensionDrop/TraceScalarization.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.JiangSuConstruction.matrixPathEquiv line 19
  2. def OAI.JiangSuConstruction.pointwiseHom line 28
  3. def OAI.JiangSuConstruction.scalarMatrixPath line 37
  4. def OAI.JiangSuConstruction.normalizedTracePath line 40
  5. lemma OAI.JiangSuConstruction.normalizedTracePath_eq line 46
  6. lemma OAI.JiangSuConstruction.scalarMatrixPath_add line 53
  7. lemma OAI.JiangSuConstruction.scalarMatrixPath_sub line 61
  8. lemma OAI.JiangSuConstruction.scalarization_ambient line 68
  9. lemma OAI.JiangSuConstruction.interior_mem line 93
  10. lemma OAI.JiangSuConstruction.leftPath_mem line 99
  11. lemma OAI.JiangSuConstruction.rightPath_mem line 105
  12. lemma OAI.JiangSuConstruction.pointwise_scalar line 111
  13. lemma OAI.JiangSuConstruction.normalizedTracePath_left line 118
  14. lemma OAI.JiangSuConstruction.normalizedTracePath_right line 129
  15. lemma OAI.JiangSuConstruction.scalarMatrixPath_apply line 152
  16. lemma OAI.JiangSuConstruction.pointwiseHom_scalarMatrixPath line 155
  17. lemma OAI.JiangSuConstruction.trace_scalarization_interior line 172
  18. lemma OAI.JiangSuConstruction.trace_scalarization_left line 185
  19. lemma OAI.JiangSuConstruction.trace_scalarization_right line 203
  20. lemma OAI.JiangSuConstruction.trace_scalarization_on_drop line 221
  21. lemma OAI.JiangSuConstruction.scalarMatrixPath_mem line 252
  22. def OAI.JiangSuConstruction.scalarDrop line 261
  23. theorem OAI.JiangSuConstruction.dimensionDrop_trace_factorization line 264