OAI/Analysis/JiangSu/DimensionDrop/DimensionDropScalarFunctions.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionDropModel.evaluation line 29
  2. def OAI.DimensionDropModel.coordinate line 37
  3. lemma OAI.DimensionDropModel.functionValues_mem line 38
  4. lemma OAI.DimensionDropModel.coordinate_mem line 40
  5. lemma OAI.DimensionDropModel.coordinate_selfadjoint line 53
  6. theorem OAI.DimensionDropModel.scalar_mem line 58
  7. def OAI.DimensionDropModel.algebraicFibre line 91
  8. lemma OAI.DimensionDropModel.phi_mem_fibre line 92
  9. lemma OAI.DimensionDropModel.s_mem_fibre line 93
  10. lemma OAI.DimensionDropModel.real_smul_mem_fibre line 94
  11. lemma OAI.DimensionDropModel.bridge_mem_fibre line 97
  12. lemma OAI.DimensionDropModel.amplify_unit_mem_fibre line 103
  13. lemma OAI.DimensionDropModel.amplify_mul_upper line 117
  14. lemma OAI.DimensionDropModel.upper_mul_amplify line 122
  15. lemma OAI.DimensionDropModel.amplify_upper_amplify line 127
  16. lemma OAI.DimensionDropModel.anchor_mul_phi line 132
  17. lemma OAI.DimensionDropModel.upper_unit_mem_fibre line 135
  18. lemma OAI.DimensionDropModel.matrix_expansion line 140
  19. lemma OAI.DimensionDropModel.mem_of_units line 144
  20. theorem OAI.DimensionDropModel.interior_generation line 150
  21. theorem OAI.DimensionDropModel.lower_generation line 158
  22. theorem OAI.DimensionDropModel.upper_generation line 161
  23. def OAI.DimensionDropModel.leftEndpoint line 181
  24. def OAI.DimensionDropModel.rightEndpoint line 182
  25. theorem OAI.DimensionDropModel.endpoint_function_mem line 183