OAI/Analysis/JiangSu/Absorption/RealUnitaryFlow.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JiangSuConstruction.realUnitaryFlow line 18
2. lemma OAI.JiangSuConstruction.realUnitaryFlow_continuous line 21
3. lemma OAI.JiangSuConstruction.realUnitaryFlow_zero line 25
4. lemma OAI.JiangSuConstruction.realUnitaryFlow_add line 28
5. lemma OAI.JiangSuConstruction.realUnitaryFlow_neg line 37
6. lemma OAI.JiangSuConstruction.realUnitaryFlow_one line 43
7. lemma OAI.JiangSuConstruction.realUnitaryFlow_commute line 47
8. lemma OAI.JiangSuConstruction.realUnitaryFlow_commute_flow line 52
9. lemma OAI.JiangSuConstruction.realUnitaryFlow_mem line 59
10. lemma OAI.JiangSuConstruction.realUnitaryFlow_period_two line 70