OAI/Analysis/DiamondDistortion/FullDual.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DiamondDistortion.RecursiveModel.exponent_real_gt_one line 19
  2. instance OAI.DiamondDistortion.RecursiveModel.vectorComponentDualSeparable line 27
  3. instance OAI.DiamondDistortion.RecursiveModel.fullVectorDualSeparable line 35
  4. instance OAI.DiamondDistortion.RecursiveModel.vectorDualSeparable line 37
  5. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.coordinate_of_equiv line 45
  6. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.transported_projection_coordinate line 53
  7. def OAI.DiamondDistortion.EquivalentNorm.Data.coordinate line 65
  8. lemma OAI.DiamondDistortion.EquivalentNorm.Data.coordinate_apply line 67
  9. lemma OAI.DiamondDistortion.EquivalentNorm.Data.coordinate_embedding line 68
  10. def OAI.DiamondDistortion.RecursiveModel.outerCoordinate line 73
  11. lemma OAI.DiamondDistortion.RecursiveModel.outerCoordinate_apply line 75
  12. lemma OAI.DiamondDistortion.RecursiveModel.outerCoordinate_embedding line 77
  13. def OAI.DiamondDistortion.PathModel.linearFullCoordinate line 85
  14. def OAI.DiamondDistortion.PathModel.quadraticFullCoordinate line 87
  15. lemma OAI.DiamondDistortion.PathModel.linearFullCoordinate_equiv line 89
  16. lemma OAI.DiamondDistortion.PathModel.quadraticFullCoordinate_equiv line 94
  17. lemma OAI.DiamondDistortion.PathModel.linearFullHeads_coordinate line 100
  18. lemma OAI.DiamondDistortion.PathModel.quadraticFullHeads_coordinate line 109
  19. def OAI.DiamondDistortion.RecursiveModel.fullVectorCoordinate line 121
  20. lemma OAI.DiamondDistortion.RecursiveModel.fullVectorCoordinate_equiv line 123
  21. lemma OAI.DiamondDistortion.RecursiveModel.fullVectorHeads_coordinate line 128
  22. def OAI.DiamondDistortion.StartModel.componentCoordinate line 141
  23. lemma OAI.DiamondDistortion.StartModel.componentCoordinate_rep line 146
  24. lemma OAI.DiamondDistortion.StartModel.componentCoordinate_embedding line 148
  25. def OAI.DiamondDistortion.StartModel.fullCoordinate line 153
  26. lemma OAI.DiamondDistortion.StartModel.fullCoordinate_embedding line 155
  27. lemma OAI.DiamondDistortion.StartModel.fullCoordinate_equiv line 157
  28. lemma OAI.DiamondDistortion.StartModel.fullHeads_coordinate line 161